proposition: Lemma Id_words_inclus : forall (E F : Ensf) (f : Word -> Word), inclus F E -> Id_words E f -> Id_words F f.
proof: Proof. intros E F f inclus_F_E Id_E_f. red in |- *. intros x inmonoid_F_x. apply Id_E_f. apply inmonoid_inclus with F; assumption. Qed.
imports: Ensf Words more_words need