proposition: Lemma Gunion_disj_Regles : isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> Regles X Vu Ru.
proof: Proof. intros. unfold Vu, Ru in |- *; simpl in |- *. apply Regles_add. apply Regles_add. apply Regles_add2. change (Regles X (fst (Gunion V1 R1 V2 R2)) (snd (Gunion V1 R1 V2 R2))) in |- *. prolog [ Gunion_Regles ] 2. auto. apply inmonoid_cons. trivial. cut (dans S2 V2); [ auto | prolog [ isGram3 ] 2 ]. auto. apply inmonoid_cons. trivial. cut (dans S1 V1); [ auto | prolog [ isGram3 ] 2 ]. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3