forall a b E x (E': a <= x /\ x <= b), Interval_restrict a b E x = exist _ x E'. Proof. intros a b E x E'. unfold Interval_restrict. apply Sigma.path_sigma_hprop. simpl. rewrite meet_l;[apply join_r|];apply E'. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.