Theorem: back_def (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : Back C α
c : C
h : ¬isEmpty c = true
⊢ some (back c h) = some ((back? c).get ⋯)
Tactic:
simpa using (back_mem c h).symm
State after:
no goals