law le_refl

lawful-words@0.1.0.0 · proof_nat.bend:634

import Base

634law le_refl:
635  for +a: Nat
636  {Nat.is_le(a, a) == True{} : Bool}