proposition: Lemma Gunion_disj_LG_inclus3 : l_inclus (LG X V2 R2 S2) (LG X Vu Ru S).
proof: Proof. red in |- *. unfold LG in |- *. intros w temp; elim temp; clear temp. intros Der_Ru inmonoid_X_w. unfold Ru in |- *; simpl in |- *. split. apply Derivestar_R with (cons S2 nil). replace (cons S2 nil) with (Append (cons S2 nil) nil). auto. auto. apply Derivestar_inclus with R2; auto. assumption. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3