congr!
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi
case h.e'_1
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) phi = phi

case h.e'_2
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) psi = psi