proposition: Lemma bin_op_is_strext_un_op_rht : forall (op : CSetoid_bin_op) (c : S), un_op_strext (fun x : S => op c x).
proof: Proof. apply bin_fun_is_strext_fun_rht. Defined.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid