proposition: Lemma id'' a : N.of_nat (N.to_nat a) = a.
proof: Proof. destruct a as [ | p]; simpl; trivial. destruct (Pos2Nat.is_succ p) as (n,H). rewrite H. simpl. f_equal. apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.id_succ. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance