Theorem: Cached.eq_of_subsingleton (YatimaStdLib/Cached.lean)

State before:
α : Sort u_1
inst✝ : Subsingleton α
a b : α
⊢ (a = b) = True
Tactic:
simp [Subsingleton.allEq a b]
State after:
no goals