simp only [Var.openList]
D : Type
V : VarAssignment D
i : ℕ
⊢ V (Var.openList 0 [] (bound_ i)) = V (bound_ i)
D : Type
V : VarAssignment D
i : ℕ
⊢ V (if i < 0 then bound_ i else if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) =
    V (bound_ i)