proposition: Lemma csbf_wd_unfolded : forall (f : CSetoid_bin_fun) (x x' : S1) (y y' : S2), x [=] x' -> y [=] y' -> f x y [=] f x' y'.
proof: Proof. Proof csbf_wd. Lemma csf_strext_unfolded : forall (f : CSetoid_fun) (x y : S1), f x [#] f y -> x [#] y. Proof csf_strext. End CSetoid_functions. Lemma bin_fun_is_wd_fun_lft : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S2), fun_wd _ _ (fun x : S1 => f x c). 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