have s1 : ¬ i + 1 < j + 1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d
case s1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ ¬i + 1 < j + 1

D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
c1 :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
s1 : ¬i + 1 < j + 1
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d