congr! 1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi) ↔
    (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'