proposition: Lemma restr_bin_op_strext : bin_op_strext Build_SubCSetoid restr_bin_op.
proof: Proof. intros x1 x2 y1 y2. case y2. case y1. case x2. case x1. intros. exact (cs_bin_op_strext _ f _ _ _ _ X). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid