proposition: Lemma bin_fun_is_strext_fun_lft : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S2), fun_strext _ _ (fun x : S1 => f x c).
proof: Proof. intros S1 S2 S3 f c x y H. cut (x [#] y or c [#] c). intros [H1|H2];auto. now set (ap_irreflexive _ c H2). eapply csbf_strext. apply H. Defined.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid