proposition: Lemma nth_nil : forall A i (d:A), nth i [] d = d.
proof: Proof. intros. unfold nth. case i; trivial. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance