proposition: Lemma IMinus_strext : forall x y : subset I, f x[-]g x [#] f y[-]g y -> x [#] y.
proof: Proof. intros x y H. elim (cg_minus_strext _ _ _ _ _ H); intro H0; exact (csf_strext_unfolded _ _ _ _ _ H0). Qed.
imports: CoRN.ftc.PartFunEquality