proposition: Lemma removePresent_In : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A) a, In a ls2 -> (~ In a ls1) -> In a (removePresent eqd ls1 ls2).
proof: Proof. induction ls2; intuition; simpl in *. intuition; subst. unfold setLet. destruct (in_dec eqd a0 ls1); intuition. unfold setLet. destruct (in_dec eqd a ls1); subst. eauto. simpl. destruct (eqd a a0); subst. intuition. right. eauto. Qed.
imports: FCF.FCF Permutation