proposition: Lemma same_order_extens : forall a b : E, same_order a b -> like a -> like b -> a = b.
proof: Proof. ir. assert (U a = U b). ap same_underlying; am. assert (leq a = leq b). ap arrow_extensionality. ir. ap arrow_extensionality. ir. ap same_leq_eq. am. uh H0. rw H0. rw H2. rw H3. sy. exact H1. Qed.
imports: universe