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