proposition: Lemma dans_map_injd : forall (e : Ensf) (x : Elt), dans x (map injdroite e) -> dans (first x) e.
proof: Proof. intros. cut (exists y : Elt, dans y e /\ x = injdroite y). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht. intros y Ht; elim Ht; clear Ht. intros. unfold injdroite in H1. replace (first x) with y; auto. symmetry in |- *. replace y with (first (couple y un)); auto. apply (f_equal (A:=Elt) (B:=Elt)); auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_couple Ensf_inclus Ensf_map