proposition: Lemma map_Id : forall (E : Ensf) (f : Elt -> Elt), Id E f -> map f E = E :>Ensf.
proof: Proof. intros E f. elim E; unfold map in |- *. auto. intros a b Hyp_rec Id_a_b_f. apply add_add. auto. apply Hyp_rec. apply Id_inclus with (add a b); auto. Qed.
imports: Ensf Words more_words need