definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
CSetoid_bin_op (mk_SubCSetoid S P) \def
\lambda S:CSetoid. \lambda P: S \to Prop.
\lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).
definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
CSetoid_bin_op (mk_SubCSetoid S P) \def
\lambda S:CSetoid. \lambda P: S \to Prop.
\lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).