def eq_le

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:216

import Base

216def eq_le(+a: Nat, +b: Nat, e: {a == b : Nat}) -> {Nat.is_le(a, b) == True{} : Bool}:
217  %e : {Nat.is_le(a, _) == True{} : Bool}
218  le_refl(a)