proposition: Lemma Derivestar_R : forall (R : Ensf) (u v w : Word), Derive R u v -> Derivestar R v w -> Derivestar R u w.
proof: Proof. unfold Derivestar in |- *. prolog [ Rstar_R ] 8. Qed.
imports: Ensf Words more_words need fonctions Relations