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