no goals
n : ℕ
α : Type u_1
v : List α
hv : List.length v = n
w : List α
hw : List.length w = n
h : ∀ (m : Fin n), get { val := v, property := hv } m = get { val := w, property := hw } m
⊢ List.length ↑{ val := v, property := hv } = List.length ↑{ val := w, property := hw }
rw [hv, hw]