def word.eq_head

bend-osdev-algo@0.1.0.0 · PROOF.bend:1023

import Base

1023def word.eq_head(c: Cmp, x: Bool, y: Bool, e: {Cmp.is_eq(Word.cmp.fin(x, y, c)) == True{} : Bool}) -> {x == y : Bool}:
1024  match c:
1025    case LT{}:
1026      Empty.absurd({x == y : Bool}, absurd.ft(e))
1027    case EQ{}:
1028      match x y:
1029        case True{} True{}:
1030          {==}
1031        case False{} False{}:
1032          {==}
1033        case True{} False{}:
1034          Empty.absurd({True{} == False{} : Bool}, absurd.ft(e))
1035        case False{} True{}:
1036          Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))
1037    case GT{}:
1038      Empty.absurd({x == y : Bool}, absurd.ft(e))