proposition: Lemma notInArrayLookupNone_unzip : forall (A B : Set)(eqd : EqDec A)(arr : Array A B) a, (~ In a (fst (unzip arr))) -> (arr # a) = None.
proof: Proof. induction arr; intuition; simpl in *. case_eq (eqb a a0); intuition. rewrite eqb_leibniz in H0. subst. intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold