proposition: Lemma Derivegstar_Derivestar : forall (X R : Ensf) (u v : Word), Derivegstar X R u v -> Derivestar R u v.
proof: Proof. unfold Derivegstar, Rstar, Derivestar in |- *. intros X R x y Derivegstar_x_y. pattern x, y in |- *. apply Derivegstar_x_y. intro. apply Rstar_reflexive. intros u v w Der Der_star. apply Rstar_R with v. apply Deriveg_Derive with X; assumption. assumption. Qed.
imports: Ensf Words fonctions Relations gram