Theorem: List.length_uniqueAux (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ length (uniqueAux xs acc) = length (unique xs) + length acc
Tactic:
rw [uniqueAux_acc_append _ _ h, length_append, length_reverse, Nat.add_comm]
State after:
no goals