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

State before:
α : Type u_1
head✝¹ head✝ : α
tl : List α
⊢ length (split' (head✝¹ :: head✝ :: tl)).2.1 = length (head✝¹ :: head✝ :: tl) / 2
Tactic:
simpa using List.split'_length_left tl
State after:
no goals