proposition: Lemma INth_strext : forall x y : subset I, f x[^]n [#] f y[^]n -> x [#] y.
proof: Proof. intros. apply csf_strext_unfolded with (IR:CSetoid) f. apply nexp_strext with n; assumption. Qed.
imports: CoRN.ftc.PartFunEquality