proposition: Theorem In_arrayLookupList : forall (A B : Set)(eqda : EqDec A)(a : A)(b : B) ls, In b (arrayLookupList _ ls a) -> exists ls', In (a, ls') ls /\ In b ls'.
proof: Proof. intuition. unfold arrayLookupList in *. case_eq (arrayLookup eqda ls a); intuition; rewrite H0 in H. eapply arrayLookup_Some_impl_In in H0. econstructor. split. eauto. trivial. simpl in *. intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold