proposition: Lemma helper: forall {A} (l0: list A) i0, S (S (length match l0 with | [] => [] | _ :: _ => i0 :: removelast l0 end)) = S (S (length l0)).
proof: Proof. intros A l0. induction l0; intros. - now simpl. - simpl. now rewrite IHl0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance