simp only [if_pos h2]
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (if i < j then bound_ i else bound_ (i + 1))
no goals