law eq_comm

lawful-words@0.1.0.0 · proof_nat.bend:1484

import Base

1484law eq_comm:
1485  for +a: Nat
1486  for +b: Nat
1487  {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}