proposition: Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'.
proof: Proof. split. apply inj. intros; now subst. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance