proposition: Lemma bin_fun_is_wd_fun_rht : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S1), fun_wd _ _ (fun x : S2 => f c x).
proof: Proof. intros S1 S2 S3 f c x y H. now apply csbf_wd; [apply eq_reflexive|]. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid