proposition: Lemma 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.
proof: Proof. intros x y Hx Hy H. exact (pfstrx _ _ _ _ _ _ (pfstrx _ _ _ _ _ _ H)). Qed.
imports: CoRN.algebra.CSetoids