no goals
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.603198
inst✝¹ : Inhabited Λ
σ : Type ?u.603204
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ (ListBlank.nth (addBottom L) (n + 1)).fst = false
rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]