simp only [Formula.openList]
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (pred_ X vs)) ↔ Formula.lc_at (j + zs.length) (pred_ X vs)
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)) ↔
    Formula.lc_at (j + zs.length) (pred_ X vs)