def un.word_eq
bend-osdev-u32@0.1.0.0 · PROOF.bend:460
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base
460def un.word_eq(n: Nat, a: Word(n), b: Word(n), +e: {Word.cmp(n, a, b) == EQ{} : Cmp}) -> {a == b : Word(n)}:
461 match n:
462 case 0n:
463 match a b:
464 case WNil{} WNil{}:
465 {==}
466 case 1n+ +p:
467 match a b:
468 case WCon{+x, +at} WCon{+y, +bt}:
469 un.wcon_eq(p, x, y, at, bt, un.fin_eq_head(Word.cmp(p, at, bt), x, y, e), un.word_eq(p, at, bt, un.fin_eq_tail(Word.cmp(p, at, bt), x, y, e)))