def eq_true

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:328

import Base

328def eq_true(+a: U32, +b: U32, +e: {a == b : U32}) -> {U32.is_eq(a, b) == True{} : Bool}:
329  %e : {U32.is_eq(a, _) == True{} : Bool}
330  eq_refl(a)