proposition: Lemma Astar_is_CSemiGroup: (is_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A)).
proof: Proof. unfold is_CSemiGroup. unfold associative. intros x. unfold app_as_csb_fun. simpl. induction x. simpl. intros x y. apply eq_fm_reflexive. simpl. intuition. Qed.
imports: CoRN.algebra.CSetoidInc