case mk
α✝ β : Type u
a✝ : Cardinal
α : Type u_1
⊢ 0 ≤ Quot.mk Setoid.r α
α β : Type u
⊢ ∀ (a : Cardinal), 0 ≤ a
rintro ⟨α⟩
no goals
case mk
α✝ β : Type u
a✝ : Cardinal
α : Type u_1
⊢ 0 ≤ Quot.mk Setoid.r α
exact ⟨Embedding.ofIsEmpty⟩