proposition: Lemma generated_group_prop_included : forall (G : GROUP) (A : part_set G), included A (generated_group A).
proof: Proof. unfold included in |- *. simpl in |- *. intros G A x H'; try assumption. exists (Var (V:=A) (Build_subtype (E:=G) (P:=A) (subtype_elt:=x) H')); split; [ idtac | try assumption ]. auto with algebra. simpl in |- *. auto with algebra. Qed.
imports: Group_kernel Free_group