proposition: Lemma IntPartIR_strext : fun_strext (fun x : subset I => F (scs_elem _ _ x) (Hf _ (scs_prf _ _ x))).
proof: Proof. red in |- *; intros x y H. generalize (pfstrx _ _ _ _ _ _ H). case x; case y; auto. Qed.
imports: CoRN.ftc.IntervalFunct