proposition: Lemma image_Regles : Regles X V1 R1 -> Regles Xim Vim Rim.
proof: Proof. unfold Rim, Vim, Xim, Gim3, Gim2, Gim, imageGram, Regles in |- *; simpl in |- *. intros R_R1 x dans_x. cut (exists x_ant : Elt, dans x_ant R1 /\ x = fonc x_ant :>Elt). intro temp; elim temp; clear temp. intros x_ant temp; elim temp; clear temp; intros x_ant_in_R1 x_egal. elim (R_R1 x_ant x_ant_in_R1). intros A_ant dans_A_ant_V1 temp; elim temp; clear temp. intros B_ant x_ant_egal inmonoid_x_ant. exists (f A_ant). apply dans_map_inv; assumption. exists (Word_ext f B_ant). rewrite x_egal; unfold fonc in |- *; unfold fet in |- *. rewrite x_ant_egal; unfold first in |- *; unfold second in |- *; unfold word_inv in |- *; simpl in |- *. trivial. replace (union (map f X) (map f V1)) with (map f (union X V1)); auto. apply dans_map; assumption. Qed.
imports: Ensf Words more_words need fonctions Relations gram