proposition: Lemma bin_part_function_comp_dom_wd : pred_wd S1 R.
proof: Proof. 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). assumption. apply bpfwdef; assumption. Qed.
imports: CoRN.algebra.CSetoids