no goals
α : Type ?u.106108
β : Type ?u.106111
γ : Type ?u.106114
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ (#↑{o' | o' < o}) = Cardinal.lift (card o)
rw [lift_card, ← type_subrel_lt, card_type]