law double_inj

bend-kit-lemmas@0.1.1.0 · lemmas.bend:197

import Base

197law double_inj:
198  for a: Nat
199  for b: Nat
200  for h: {Nat.double(a) == Nat.double(b) : Nat}
201  {a == b : Nat}