~/jendhub

def cmp_refl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:90

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as Natcmp
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

90def cmp_refl(+a: Nat) -> {Nat.cmp(a, a) == EQ{} : Cmp}:
91  eq_c(Nat.cmp(a, a), N.is_eq_refl(a))

Uses (5)

Used by (1)