no goals
α : Type ?u.219643
β : Type ?u.219646
γ : Type ?u.219649
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ principalSeg.top = type fun x x_1 => x < x_1
simp only [lift.principalSeg_top, univ_id]