Theorem: Lean.PersistentArray.WF.toList'_length (Lean4Lean/Verify/Axioms.lean)

State before:
α✝ : Type u_1
arr : PersistentArray α✝
h : WF arr
⊢ List.length (toList' arr) = arr.size
Tactic:
induction h <;> simp [*]
State after:
no goals