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

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