fact: Record BinPartFunct (S1 S2 : CSetoid) : Type := {bpfdom : S1 -> CProp; bdom_wd : pred_wd S1 bpfdom; bpfpfun :> forall x : S1, bpfdom x -> S2; bpfstrx : forall x y Hx Hy, bpfpfun x Hx [#] bpfpfun y Hy -> x [#] y}.
imports: CoRN.algebra.CSetoids