proposition: Theorem arrayLookup_Some_In_split: forall (A B : Set) (eqd : EqDec A) (arr : list (A * B)) (a : A) (b : B), arrayLookup eqd arr a = Some b -> In a (fst (split arr)).
proof: Proof. induction arr; intuition; simpl in *. discriminate. remember (split arr) as z. destruct z. simpl. case_eq (eqb a a0); intuition. rewrite eqb_leibniz in H0. intuition. rewrite H0 in H. right. eapply IHarr; intuition. eauto. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv