proposition: Lemma pair_eq_inv : forall (A B : Type)(a1 a2 : A)(b1 b2 : B), (a1, b1) = (a2, b2) -> a1 = a2 /\ b1 = b2.
proof: Proof. intros. inversion H; clear H; subst. intuition. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation