proposition: Lemma Gunion_Regles : isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> Regles X Vu Ru.
proof: Proof. intros. unfold Ru in |- *; unfold C in |- *; unfold Gunion in |- *; simpl in |- *. apply Regles_union; unfold Vu in |- *; unfold C in |- *; unfold Gunion in |- *; simpl in |- *. apply Regles_V with V1; [ auto | apply isGram4 with S1; auto ]. apply Regles_V with V2; [ auto | apply isGram4 with S2; auto ]. Qed.
imports: Ensf Words more_words need fonctions Relations gram