~/jendhub

def un.cmp_refl

bend-osdev-u32@0.1.0.0 · PROOF.bend:271

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base

271def un.cmp_refl(a: Nat) -> {Nat.cmp(a, a) == EQ{} : Cmp}:
272  match a:
273    case 0n:
274      {==}
275    case 1n+p:
276      un.cmp_refl(p)

Uses (3)

Used by (1)