proposition: Lemma comp_Rf : forall (g f : Elt -> Elt) (x : Elt), dans x R -> comp (Rf g) (Rf f) x = Rf (comp g f) x :>Elt.
proof: Proof. clear Mono. intros f' g x dans_x_R. elim (Regles_X_V_R x dans_x_R). intros A dans_A_V temp. elim temp; clear temp; intros B egal_x inmonoid_B. rewrite egal_x. unfold Rf in |- *. unfold comp at 1 in |- *. apply couple_couple. apply refl_equal. simpl in |- *. rewrite (comp_Word_ext f' g B). apply refl_equal. Qed.
imports: Ensf Words more_words need fonctions Relations gram gram2