proposition: Lemma dans_add : forall (x y : Elt) (e : Ensf), dans x (add y e) -> y = x \/ dans x e.
proof: Proof. intros x y e H. simple inversion H. left. injection H1. intros. apply trans_equal with x0; [ auto | assumption ]. intro. right. injection H2. intros. rewrite <- H3. rewrite <- H1. assumption. Qed.
imports: Ensf_types