proposition: Theorem notInArrayLookupNone: forall (A B : Set) (eqd : EqDec A) (arr : Array A B) (a : A), ~ In a (fst (split arr)) -> arrayLookup eqd arr a = None.
proof: Proof. induction arr; intuition; simpl in *. remember (split arr) as z. destruct z. simpl in *. intuition idtac. case_eq (eqb a a0); intros. rewrite eqb_leibniz in H. subst. intuition idtac. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold