proposition: Lemma bin_fun_is_strext_fun_rht : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S1), fun_strext _ _ (fun x : S2 => f c x).
proof: Proof. intros S1 S2 S3 op c x y H. cut (c [#] c or x [#] y). intro Hv. elim Hv. intro Hf. generalize (ap_irreflexive _ c Hf). tauto. auto. eapply csbf_strext. apply H. Defined.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid