no goals
K : Type u_1
inst✝² : DecidableEq K
Γ : K → Type u_2
Λ : Type ?u.605156
inst✝¹ : Inhabited Λ
σ : Type ?u.605162
inst✝ : Inhabited σ
L : ListBlank ((k : K) → Option (Γ k))
⊢ (ListBlank.head (addBottom L)).fst = true
rw [addBottom, ListBlank.head_cons]