cases h2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))