α : Type ?u.230240
β : Type ?u.230243
γ : Type ?u.230246
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
x : (Quotient.out (ord c)).α
⊢ typein (fun x x_1 => x < x_1) x < ord c
α : Type ?u.230240
β : Type ?u.230243
γ : Type ?u.230246
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
x : (Quotient.out (ord c)).α
⊢ card (typein (fun x x_1 => x < x_1) x) < c
rw [← lt_ord]
no goals
α : Type ?u.230240
β : Type ?u.230243
γ : Type ?u.230246
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
x : (Quotient.out (ord c)).α
⊢ typein (fun x x_1 => x < x_1) x < ord c
apply typein_lt_self