proposition: Lemma Derivestar_inclus : forall (R1 R2 : Ensf) (u v : Word), inclus R1 R2 -> Derivestar R1 u v -> Derivestar R2 u v.
proof: Proof. intros R1 R2 u v inclus_R1_R2 Der_R1. unfold Derivestar, Rstar in Der_R1. pattern u, v in |- *. apply Der_R1. auto. intros; prolog [ Derive_inclus Derivestar_R ] 3. Qed.
imports: Ensf Words more_words need fonctions Relations