no goals
α : Type u_1
β : Type ?u.240276
γ : Type ?u.240279
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ type r = ↑(Fintype.card α)
rw [← card_eq_nat, card_type, mk_fintype]