no goals
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α
constructor <;> exact inferInstance
α : Sort u
x✝ : Subsingleton α ∧ Nonempty α
hs : Subsingleton α
hn : Nonempty α
inhabited_h : Inhabited α
⊢ Unique α
α : Sort u
x✝ : Subsingleton α ∧ Nonempty α
hs : Subsingleton α
hn : Nonempty α
⊢ Unique α
inhabit α
no goals
α : Sort u
x✝ : Subsingleton α ∧ Nonempty α
hs : Subsingleton α
hn : Nonempty α
inhabited_h : Inhabited α
⊢ Unique α
exact Unique.mk' α