proposition: Theorem arrayLookupOpt_getSomes_eq : forall (A B : Set)(eqda : EqDec A)(ls : list (option (A * B)))(a : A), arrayLookupOpt _ ls a = arrayLookup _ (getSomes ls) a.
proof: Proof. induction ls; intuition; simpl in *. destruct a. destruct p. simpl. case_eq (eqb a0 a); intuition. eapply IHls. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold