proposition: Theorem any_dec_in_dec_swap : forall (A : Set)(eqda : EqDec A)(ls1 ls2 : list A), any_dec (fun x => if (in_dec (EqDec_dec _) x ls2) then true else false) ls1 = any_dec (fun x => if (in_dec (EqDec_dec _) x ls1) then true else false) ls2.
proof: Proof. induction ls1; intuition idtac; simpl in *. destruct ls2; simpl in *. trivial. rewrite any_dec_cons. simpl. unfold any_dec. simpl. symmetry. apply fold_left_orb_all_false. rewrite any_dec_cons. destruct (in_dec (EqDec_dec eqda) a ls2). simpl. symmetry. eapply ex_any_dec. eauto. destruct (EqDec_dec eqda a a). trivial. intuition eauto. simpl. rewrite IHls1. eapply any_dec_f_eq. intuition idtac. destruct (EqDec_dec eqda a a0). subst. intuition idtac. destruct (in_dec (EqDec_dec eqda) a0 ls1); trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation