proposition: Lemma generated_monoid_prop : forall (M : MONOID) (A : part_set M) (y : M), in_part y (generated_monoid A) -> exists x : FM A, Equal y (FM_lift (inj_part A) x).
proof: Proof. simpl in |- *; auto with algebra. intros M A y H'; try assumption. elim H'; intros x E; elim E; intros H'0 H'1; try exact H'1; clear E H'. exists x; try assumption. Qed.
imports: Monoid_kernel Free_monoid