law dbl_inj

lawful-words@0.1.0.0 · proof_nat.bend:553

import Base

553law dbl_inj:
554  for +x: Nat
555  for +y: Nat
556  for e: {Nat.double(x) == Nat.double(y) : Nat}
557  {x == y : Nat}