congr! 1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
⊢ Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi

case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
h1_left : NotFree Γ v phi
h1_right : NotFree Γ v psi
a✝ : Holds D I (Function.updateITE V v d) M E phi
⊢ Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi