simp only [Function.updateITE_comp_right σ' σ.1 V v d h1_left h1_right]
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE V v d ∘ σ') M E (τ X)
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ Γ' : List (VarName × MetaVarName)
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ' → IsNotFree D I M E (meta_var_ X) v
h3 : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → NotFree Γ' (↑σ v) (τ X)
v : VarName
X : MetaVarName
a1 : (v, X) ∈ Γ
V : Valuation D
d : D
h1_left : ↑σ ∘ σ' = id
h1_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ σ') M E (τ X) ↔ Holds D I (Function.updateITE (V ∘ σ') (↑σ v) d) M E (τ X)