Theorem: isEmpty_eq_decide_size (Algorithm/Data/Classes/Size.lean)

State before:
C : Type u_1
α : Type ?u.565
inst✝ : Size C
c : C
⊢ isEmpty c = decide (size c = 0)
Tactic:
simp only [← isEmpty_iff_size_eq_zero, Bool.decide_coe]
State after:
no goals