rw [f_preserves_size assignments' a, hsize]
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
assignments' : Array Assignment
hsize : assignments'.size = assignments.size
a : α
x✝ : a ∈ l
⊢ (f assignments' a).size = assignments.size
no goals