α : Type u_1
β : Type ?u.2650
h : Subsingleton α
⊢ ∀ (x y : α), x = y
α : Type u_1
β : Type ?u.2650
⊢ Subsingleton α → ∀ (x y : α), x = y
intro h
no goals
α : Type u_1
β : Type ?u.2650
h : Subsingleton α
⊢ ∀ (x y : α), x = y
exact Subsingleton.elim