proposition: Lemma Id_image_X : Id (union X V1) f -> Xim = X :>Ensf.
proof: Proof. unfold Xim, Gim, imageGram in |- *; simpl in |- *. elim X. auto. intros a X' Hyp Id_a_X_V1_f. unfold map in |- *. simpl in |- *. apply add_add. auto. apply Hyp. apply Id_inclus with (union (add a X') V1). red in |- *; intros x dans_x_union_X_V1. cut (dans x X' \/ dans x V1). intros [HX| HV1]; auto. auto. assumption. Qed.
imports: Ensf Words more_words need fonctions Relations gram