unfold Function.updateITE
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
⊢ Function.updateITE V h1_x (V h1_y) h1_x = Function.updateITE V h1_x (V h1_y) h1_y
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
⊢ (if h1_x = h1_x then V h1_y else V h1_x) = if h1_y = h1_x then V h1_y else V h1_y