proposition: Lemma Id_image_R : Id (union X V1) f -> isGram X V1 R1 S1 -> Rim = R1 :>Ensf.
proof: Proof. intros Id_X_V1_f. unfold Rim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *. elim R1. auto. intros a R Hyp isGram_X_V1_R1_S1. unfold map in |- *. simpl in |- *. apply add_add. cut (Regles X V1 (add a R)). unfold Regles in |- *. intro R_a_R. elim (R_a_R a). intros x dans_x_V1 temp; elim temp; clear temp. intros B egal_a inmonoid_B. rewrite egal_a. apply couple_couple; unfold first, second, word_inv in |- *; simpl in |- *. auto. apply word_word. cut (Id_words (union X V1) (Word_ext f)); auto. trivial. apply isGram4 with S1; trivial. prolog [ isGram_inclus3 ] 3. Qed.
imports: Ensf Words more_words need fonctions Relations gram