proposition: Lemma inmonoid_inclus : forall (E F : Ensf) (x : Word), inclus E F -> inmonoid E x -> inmonoid F x.
proof: Proof. intros E F x inclus_E_F inmonoid_E_x. elim inmonoid_E_x. trivial. intros w e inmonoid_E_w inmonoid_F_w dans_e_E. apply inmonoid_cons; [ assumption | apply inclus_E_F; assumption ]. Qed.
imports: Ensf