Interval_restrict@{} (a b : A) (E : a <= b) : A -> Interval a b. Proof. intros x. exists (join a (meet x b)). split. - apply join_ub_l. - apply join_le. + exact E. + apply meet_lb_r. Defined.
Require Import Import NatPair.Instances. Import Quoting.Instances.