proposition: Lemma csbf_wd : forall f : CSetoid_bin_fun, bin_fun_wd f.
proof: Proof. intro f. apply: bin_fun_strext_imp_wd. apply csbf_strext. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid