def wd.refl

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:152

import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder

import Base

152def wd.refl(n: Nat, a: Word(n)) -> {Word.cmp(n, a, a) == EQ{} : Cmp}:
153  match n:
154    case 0n:
155      {==}
156    case 1n+ +p:
157      match a:
158        case WCon{+x, +at}:
159          %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, wd.refl(p, at)) : {Word.cmp.fin(x, x, _) == EQ{} : Cmp}
160          wd.fin_refl(x)

Uses (8)

Used by (3)