proposition: Lemma helper2: forall {A} (l: list A) a, Datatypes.length (l ++ [a]) = S (Datatypes.length l).
proof: Proof. intros A l. induction l; intros. - now simpl. - simpl. now rewrite IHl. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance