law eq_refl

lawful-words@0.1.0.0 · proof_nat.bend:142

import Base

142law eq_refl:
143  for +n: Nat
144  {Nat.is_eq(n, n) == True{} : Bool}