proposition: Theorem removePresent_in_only_if : forall (A : Set)(eqd : eq_dec A)(u ls : list A) a, In a (removePresent eqd u ls) -> In a ls.
proof: Proof. induction ls; intuition; simpl in *. unfold setLet in *. destruct (in_dec eqd a u); intuition. simpl in *. intuition. Qed.
imports: FCF.FCF Permutation