proposition: Lemma nth_eq1: forall i a xs, nth (S i) (a :: xs) 1 = nth i xs 1.
proof: Proof. intros. now simpl. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance