proposition: Lemma bin_op_is_wd_un_op_rht : forall (op : CSetoid_bin_op) (c : S), un_op_wd (fun x : S => op c x).
proof: Proof. apply bin_fun_is_wd_fun_rht. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid