proposition: Lemma arrayLookup_Some_In_unzip : forall (A B : Set)(eqd : EqDec A)(arr : Array A B) a b, (arr # a) = Some b -> In a (fst (unzip arr)).
proof: Proof. induction arr; intuition; simpl in *. discriminate. case_eq (eqb a a0); intuition; rewrite H0 in *. inversion H; clear H; subst. rewrite eqb_leibniz in H0. subst. intuition. right. eapply IHarr. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold