proposition: Lemma dans_add_contr : forall (x y : Elt) (e : Ensf), y <> x -> ~ dans x e -> ~ dans x (add y e).
proof: Proof. intros; red in |- *; intro. absurd (y = x \/ dans x e). 2: apply dans_add; auto. red in |- *. intro. elim H2; auto. Qed.
imports: Ensf_types