proposition: Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'.
proof: Proof. intro H. rewrite <- (id'' a), <- (id'' a'). now f_equal. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance