proposition: Lemma Id_image_V : Id (union X V1) f -> Vim = V1 :>Ensf.
proof: Proof. unfold Vim, Gim2, Gim, imageGram; simpl in |- *. generalize V1; clearbody C Gim; clear V1. simple induction V1; auto. intros a V1' Hyp Id_X_a_V1_f. unfold map in |- *. simpl in |- *. apply add_add. auto. apply Hyp. apply Id_inclus with (union X (add a 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