Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F F' : Formula
h1 : IsSub F v t F'
⊢ Holds D I (Function.updateITE V v (V t)) E F ↔ Holds D I V E F'
Tactic:
induction h1 generalizing V
Proof state after:
case pred_const_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (pred_const_ X✝ xs✝) ↔
    Holds D I V E (pred_const_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝))

case pred_var_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (pred_var_ X✝ xs✝) ↔
    Holds D I V E (pred_var_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝))

case eq_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
x✝ y✝ v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (eq_ x✝ y✝) ↔
    Holds D I V E (eq_ (if v✝ = x✝ then t✝ else x✝) (if v✝ = y✝ then t✝ else y✝))

case true_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E true_ ↔ Holds D I V E true_

case false_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E false_ ↔ Holds D I V E false_

case not_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝.not_ ↔ Holds D I V E phi'✝.not_

case imp_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (phi✝.imp_ psi✝) ↔ Holds D I V E (phi'✝.imp_ psi'✝)

case and_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (phi✝.and_ psi✝) ↔ Holds D I V E (phi'✝.and_ psi'✝)

case or_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (phi✝.or_ psi✝) ↔ Holds D I V E (phi'✝.or_ psi'✝)

case iff_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (phi✝.iff_ psi✝) ↔ Holds D I V E (phi'✝.iff_ psi'✝)

case forall_not_free_in
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (forall_ x✝ phi✝)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (forall_ x✝ phi✝) ↔ Holds D I V E (forall_ x✝ phi✝)

case forall_free_in
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (forall_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (forall_ x✝ phi✝) ↔ Holds D I V E (forall_ x✝ phi'✝)

case exists_not_free_in
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (exists_ x✝ phi✝)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (exists_ x✝ phi✝) ↔ Holds D I V E (exists_ x✝ phi✝)

case exists_free_in
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (exists_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V v✝ (V t✝)) E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (exists_ x✝ phi✝) ↔ Holds D I V E (exists_ x✝ phi'✝)

case def_
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E (def_ X✝ xs✝) ↔
    Holds D I V E (def_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝))