proposition: Lemma filter_NoDup_perm : forall (A : Set)(eqd: eq_dec A) u ls, NoDup ls -> NoDup u -> (forall a, In a ls -> In a u) -> Permutation (filter (fun a => if (in_dec eqd a ls) then true else false) u) ls.
proof: Proof. induction u; intuition; simpl in *. destruct ls. econstructor. specialize (H1 a); simpl in *. intuition. inversion H0; clear H0; subst. destruct (in_dec eqd a ls). symmetry. eapply perm_trans. eapply (removeFirst_permutation eqd). eauto. eapply perm_skip. eapply Permutation_sym. erewrite filter_eq. eapply IHu; intuition. eapply removeFirst_NoDup. trivial. specialize (H1 a0). intuition. edestruct H1. eapply removeFirst_in_iff. eauto. subst. exfalso. eapply removeFirst_NoDup_not_in. eapply H. eauto. trivial. intuition. destruct (in_dec eqd a0 ls). destruct (in_dec eqd a0 (removeFirst eqd ls a)). trivial. exfalso. destruct (eqd a a0); subst. intuition. eapply n0. eapply removeFirst_in; eauto. destruct (in_dec eqd a0 (removeFirst eqd ls a)). exfalso. eapply removeFirst_not_in; eauto. trivial. eapply IHu; intuition. specialize (H1 a0); intuition. subst. intuition. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF