unfold.unfold.intros 2.elim x 2.elim y 2.
simplify.
intro.
-reduce in H2.
+normalize in H2.
apply (un_op_wd_unfolded ? f ? ? H2).
qed.
\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
intros.unfold.unfold. intros 2.elim y 2. elim x 2.
-intros.reduce in H2.
+intros.normalize in H2.
apply (cs_un_op_strext ? f ? ? H2).
qed.
unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
simplify.
intros.
-reduce in H4.
-reduce in H5.
+normalize in H4.
+normalize in H5.
apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
qed.
bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
simplify.intros.
-reduce in H4.
+normalize in H4.
apply (cs_bin_op_strext ? f ? ? ? ? H4).
qed.