proposition: Lemma inmon_Der_imp_inmon_R1 : forall u v : Word, Regles X V1 R1 -> Derive R1 u v -> inmonoid (union X V1) u -> inmonoid (union X V1) v.
proof: Proof. intros. apply in_mon_X_Der_imp_inmon_X with R1 u; assumption. Qed.
imports: Ensf Words more_words need fonctions Relations gram