apply a1 d
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
a1 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_psi
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_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
a1 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi