-Let R x := {Hx : P x | Q (F x Hx)}.
-
-Lemma bin_part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
- G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
-intros x y Hx Hy H.
-exact (bpfstrx _ _ _ _ _ _ _ (bpfstrx _ _ _ _ _ _ _ H)).
-Qed.
-
-Lemma bin_part_function_comp_dom_wd : pred_wd S1 R.
-red in |- *; intros x y H H0.
-unfold R in |- *; inversion_clear H.
-exists (bdom_wd _ _ F x y x0 H0).
-apply (bdom_wd _ _ G) with (F x x0).
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+definition BP : \forall S1,S2:CSetoid. \forall F: BinPartFunct S1 S2. ? \def
+ \lambda S1,S2:CSetoid. \lambda F: BinPartFunct S1 S2.
+ bpfdom ? ? F.
+(* Let P := Dom F. *)
+definition BQ : \forall S2,S3:CSetoid. \forall G: BinPartFunct S2 S3. ? \def
+ \lambda S2,S3:CSetoid. \lambda G: BinPartFunct S2 S3.
+ bpfdom ? ? G.
+(* Let Q := BDom G.*)
+definition BR : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2.
+\forall G: BinPartFunct S2 S3.
+ \forall x: ?. ? \def
+ \lambda S1,S2,S3:CSetoid. \lambda F: BinPartFunct S1 S2.
+ \lambda G: BinPartFunct S2 S3. \lambda x: ?.
+ (sigT ? (\lambda Hx : BP S1 S2 F x. BQ S2 S3 G (bpfpfun S1 S2 F x Hx))).
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+lemma bin_part_function_comp_strext : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2.
+\forall G: BinPartFunct S2 S3. \forall x,y. \forall Hx : BR S1 S2 S3 F G x.
+\forall Hy : (BR S1 S2 S3 F G y).
+(bpfpfun ? ? G (bpfpfun ? ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)) \neq
+(bpfpfun ? ? G (bpfpfun ? ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y.
+intros (S1 S2 S3 x y Hx Hy H).
+exact (bpfstrx ? ? ? ? ? ? ? (bpfstrx ? ? ? ? ? ? ? H1)).
+qed.
+
+lemma bin_part_function_comp_dom_wd : \forall S1,S2,S3:CSetoid.
+ \forall F: BinPartFunct S1 S2. \forall G: BinPartFunct S2 S3.
+ pred_wd ? (BR S1 S2 S3 F G).
+intros.
+unfold.intros (x y H H0).
+unfold BR; elim H 0.intros (x0).
+apply (existT ? ? (bdom_wd ? ? F x y x0 H0)).
+apply (bdom_wd ? ? G (bpfpfun ? ? F x x0)).