cases z
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
z : Var
a3_left : z ∈ vs
a3_right : Var.openList j (List.map free_ zs) z = bound_ i
a1 : Var.lc_at (j + zs.length) z
⊢ i < j
case free_
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a✝ : String
a3_left : free_ a✝ ∈ vs
a3_right : Var.openList j (List.map free_ zs) (free_ a✝) = bound_ i
a1 : Var.lc_at (j + zs.length) (free_ a✝)
⊢ i < j

case bound_
X : String
vs : List Var
j : ℕ
zs : List String
i a✝ : ℕ
a3_left : bound_ a✝ ∈ vs
a3_right : Var.openList j (List.map free_ zs) (bound_ a✝) = bound_ i
a1 : Var.lc_at (j + zs.length) (bound_ a✝)
⊢ i < j