proposition: Lemma restr_un_op_strext : un_op_strext Build_SubCSetoid restr_un_op.
proof: Proof. intros x y. case y. case x. intros. exact (cs_un_op_strext _ f _ _ X). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid