proposition: Lemma inmon_Der_imp_inmon_2 : forall u v : Word, isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> inter V1 V2 empty -> inmonoid (union X V2) u -> Derive Ru u v -> inmonoid (union X V2) v.
proof: Proof. intros; prolog [ inmon_Der_imp_inmon_R2 sym_inter isGram2 inter_union isGram4 inmon_Der_imp_Der2 ] 5. Qed.
imports: Ensf Words more_words need fonctions Relations gram