proposition: Lemma tailOpt_eq : forall (A : Set)(n : nat)(v1 v2 : Vector.t A n), v1 = v2 -> tailOpt v1 = tailOpt v2.
proof: Proof. intuition. subst. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation