proposition: Lemma Derive_inclus : forall (R1 R2 : Ensf) (u v : Word), inclus R1 R2 -> Derive R1 u v -> Derive R2 u v.
proof: Proof. intros R1 R2 u v inclus_R1_R2 Der_R1. elim Der_R1; auto. Qed.
imports: Ensf Words more_words need fonctions Relations