proposition: Theorem any_dec_arrayLookup_swap : forall (A B : Set)(eqda : EqDec A)(ls1 ls2 : list (A * B)), any_dec (fun x => if (arrayLookup _ ls1 x) then true else false) (fst (split ls2)) = any_dec (fun x => if (arrayLookup _ ls2 x) then true else false) (fst (split ls1)).
proof: Proof. unfold any_dec in *. induction ls1; intuition idtac; simpl in *. eapply fold_left_orb_all_false. remember (split ls1) as z. destruct z. simpl in *. case_eq (arrayLookup eqda ls2 a0); intros. rewrite fold_left_orb_true. eapply (fold_left_orb_ex). rewrite eqb_refl. trivial. eapply arrayLookup_In_split. eauto. rewrite <- IHls1. eapply fold_left_f_eq. intuition. case_eq (eqb b0 a0); intros. rewrite eqb_leibniz in H1. subst. exfalso. eapply arrayLookup_None_not_In; eauto. reflexivity. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid