proposition: Lemma generated_monoid_prop_included : forall (M : MONOID) (A : part_set M), included A (generated_monoid A).
proof: Proof. unfold included in |- *. simpl in |- *. intros M A x H'; try assumption. exists (Var (V:=A) (Build_subtype (E:=M) (P:=A) (subtype_elt:=x) H')); split; [ idtac | try assumption ]. auto with algebra. simpl in |- *. auto with algebra. Qed.
imports: Monoid_kernel Free_monoid