proposition: Lemma IComp_strext : forall x y : subset I, g (Build_subcsetoid_crr _ _ _ (Hfg x)) [#] g (Build_subcsetoid_crr _ _ _ (Hfg y)) -> x [#] y.
proof: Proof. intros x y H. apply csf_strext_unfolded with (IR:CSetoid) f. exact (csf_strext_unfolded _ _ _ _ _ H). Qed.
imports: CoRN.ftc.PartFunEquality