simp only [h2_left]
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)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)
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)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ id) M E (τ X) ↔ Holds D I V M E (τ X)