Theorem: List.split'_isSome (HMem/Complexity/BitTree.lean)

State before:
α : Type u_1
head✝¹ head✝ : α
tl : List α
⊢ Option.isSome (split' (head✝¹ :: head✝ :: tl)).1 = decide (length (head✝¹ :: head✝ :: tl) % 2 = 1)
Tactic:
simpa using List.split'_isSome tl
State after:
no goals