no goals
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.602019
inst✝¹ : Inhabited Λ
σ : Type ?u.602025
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ (ListBlank.nth (addBottom L) n).snd = ListBlank.nth L n
conv => rhs; rw [← addBottom_map L, ListBlank.nth_map]