proposition: Lemma Derivestar_image : forall u v : Word, Derivestar R1 u v -> Derivestar Rim (wef u) (wef v).
proof: Proof. unfold Derivestar in |- *. intros u v Hyp. unfold Derivestar, Rstar in Hyp. pattern u, v in |- *. apply Hyp. auto. intros a b c DeriveR1 Rst. apply Rstar_R with (y := wef b); auto. Qed.
imports: Ensf Words more_words need fonctions Relations gram