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