unfold IsMetaVarOrAllDefInEnv at h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))