case pred_ X vs =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  simp
  apply List.map_mem_id
  intro v a1
  specialize h1 v a1
  cases v
  case _ x =>
    simp only [Var.openList]
  case _ i =>
    cases i
    case zero =>
      simp only [Var.lc_at] at h1
      simp only [Var.openList]
      simp only [if_pos h1]
    case succ i =>
      simp only [Var.lc_at] at h1
      simp only [Var.openList]
      simp only [if_pos h1]
zs : List String
X : String
vs : List Var
j : ℕ
h1 : lc_at j (pred_ X vs)
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
no goals