no goals
α : Type ?u.233635
β : Type ?u.233638
γ : Type ?u.233641
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
⊢ lift c < univ
simpa only [lift.principalSeg_coe, lift_ord, lift_succ, ord_le, succ_le_iff] using
  le_of_lt (lift.principalSeg.{u, u + 1}.lt_top (succ c).ord)