proposition: Lemma Derivestar_inv : forall (R : Ensf) (u v : Word), Derivestar R u v -> u = v \/ (exists2 w : Word, Derive R u w & Derivestar R w v).
proof: Proof. unfold Derivestar in |- *. prolog [ Rstar_inv ] 6. Qed.
imports: Ensf Words more_words need fonctions Relations