law eq_sound

lawful-words@0.1.0.0 · proof_nat.bend:164

import Base

164law eq_sound:
165  for +a: Nat
166  for +b: Nat
167  for e: {Nat.is_eq(a, b) == True{} : Bool}
168  {a == b : Nat}