proposition: Lemma inmon_Der_imp_inmon_R2 : forall u v : Word, Regles X V2 R2 -> Derive R2 u v -> inmonoid (union X V2) u -> inmonoid (union X V2) v.
proof: Proof. intros u v Regles_R2 Der_R2. elim Der_R2. intros; prolog [ inmonoid_cons_inv Regles_inv2 inmonoid_Append ] 3. intros; prolog [ inmonoid_cons_inv2 inmonoid_cons_inv inmonoid_cons ] 4. Qed.
imports: Ensf Words more_words need fonctions Relations gram