cases v
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
case mp.free_
X : String
vs : List Var
j : ℕ
zs : List String
a✝ : String
a2 : free_ a✝ ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (free_ a✝))
⊢ Var.lc_at (j + zs.length) (free_ a✝)

case mp.bound_
X : String
vs : List Var
j : ℕ
zs : List String
a✝ : ℕ
a2 : bound_ a✝ ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (bound_ a✝))
⊢ Var.lc_at (j + zs.length) (bound_ a✝)