proposition: Lemma opt_eq_inv : forall (A : Type)(a1 a2 : A), Some a1 = Some a2 -> a1 = a2.
proof: Proof. intuition. inversion H; clear H; subst. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation