Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem (FOL/NV/Sub/Var/One/Ind/Sub.lean)

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
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✝))

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (pred_var_ h1_X h1_xs) ↔
    Holds D I V E (pred_var_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
case pred_const_ h1_X h1_xs h1_v h1_t | pred_var_ h1_X h1_xs h1_v h1_t =>
  simp only [Holds]
  congr! 1
  simp
  simp only [List.map_eq_map_iff]
  intro x _
  simp only [Function.updateITE]
  simp only [eq_comm]
  split_ifs
  case _ c1 =>
    simp
    simp only [if_pos c1]
  case _ c1 =>
    simp
    simp only [if_neg c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (eq_ h1_x h1_y) ↔
    Holds D I V E (eq_ (if h1_v = h1_x then h1_t else h1_x) (if h1_v = h1_y then h1_t else h1_y))
Tactic:
case eq_ h1_x h1_y h1_v h1_t =>
  simp only [Holds]
  simp only [Function.updateITE]
  simp only [eq_comm]
  congr! 1 <;> { split_ifs <;> rfl }
State after:
no goals

State before:
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_
Tactic:
case true_ _ _ | false_ _ _ =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
case not_ h1_phi h1_v h1_t h1_phi' _ h1_ih =>
  simp only [Holds]
  congr! 1
  apply h1_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬isFreeIn h1_v (exists_ h1_x h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
case
  forall_not_free_in h1_x h1_phi h1_v h1_t h1_1
| exists_not_free_in h1_x h1_phi h1_v h1_t h1_1 =>
  simp only [isFreeIn] at h1_1
  simp at h1_1
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply Holds_coincide_Var
  intro x a1
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    rfl
  case _ c1 c2 =>
    subst c2
    tauto
  case _ c1 c2 =>
    rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : isFreeIn h1_v (exists_ h1_x h1_phi)
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
Tactic:
case
  forall_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 h1_2 _ h1_ih
| exists_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 h1_2 _ h1_ih =>
  simp only [isFreeIn] at h1_1
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  specialize h1_ih (Function.updateITE V h1_x d)
  simp only [← h1_ih]
  apply Holds_coincide_Var
  intro x _
  simp only [Function.updateITE]
  simp only [eq_comm]
  split_ifs
  case _ c1 c2 c3 =>
    subst c2
    cases h1_1
    case intro h1_1_left h1_1_right =>
      contradiction
  case _ | _ | _ =>
    rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (pred_var_ h1_X h1_xs) ↔
    Holds D I V E (pred_var_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ I.pred_var_ h1_X (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) ↔
    I.pred_var_ h1_X (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ I.pred_var_ h1_X (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) ↔
    I.pred_var_ h1_X (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
congr! 1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs =
    List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)

State before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs =
    List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)
Tactic:
simp
State after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs

State before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
intro x _
State after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp only [Function.updateITE]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if x = h1_v then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if x = h1_v then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp only [eq_comm]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
h✝ : h1_v = x
⊢ V h1_t = (V ∘ fun x => if h1_v = x then h1_t else x) x

case neg
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
h✝ : ¬h1_v = x
⊢ V x = (V ∘ fun x => if h1_v = x then h1_t else x) x

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
case _ c1 =>
  simp
  simp only [if_pos c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
case _ c1 =>
  simp
  simp only [if_neg c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = V (if h1_v = x then h1_t else x)

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = V (if h1_v = x then h1_t else x)
Tactic:
simp only [if_pos c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = V (if h1_v = x then h1_t else x)

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = V (if h1_v = x then h1_t else x)
Tactic:
simp only [if_neg c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (eq_ h1_x h1_y) ↔
    Holds D I V E (eq_ (if h1_v = h1_x then h1_t else h1_x) (if h1_v = h1_y then h1_t else h1_y))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Function.updateITE V h1_v (V h1_t) h1_x = Function.updateITE V h1_v (V h1_t) h1_y ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Function.updateITE V h1_v (V h1_t) h1_x = Function.updateITE V h1_v (V h1_t) h1_y ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)
Tactic:
simp only [Function.updateITE]
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)
Tactic:
simp only [eq_comm]
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_x = h1_v then h1_t else h1_x) = V (if h1_y = h1_v then h1_t else h1_y)

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_x = h1_v then h1_t else h1_x) = V (if h1_y = h1_v then h1_t else h1_y)
Tactic:
congr! 1 <;> { split_ifs <;> rfl }
State after:
no goals

State before:
case a.h.e'_3
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ (if h1_y = h1_v then V h1_t else V h1_y) = V (if h1_y = h1_v then h1_t else h1_y)
Tactic:
split_ifs <;> rfl
State after:
no goals

State before:
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_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ ¬Holds D I V E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ ¬Holds D I V E h1_phi'
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
apply h1_ih
State after:
no goals

State before:
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.iff_ h1_psi) ↔ Holds D I V E (h1_phi'.iff_ h1_psi')
Tactic:
simp only [Holds]
State after:
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')

State before:
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')
Tactic:
congr! 1
State after:
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'

State before:
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'
Tactic:
apply h1_ih_1
State after:
no goals

State before:
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'
Tactic:
apply h1_ih_2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬isFreeIn h1_v (exists_ h1_x h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
simp only [isFreeIn] at h1_1
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬(¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬(¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
simp at h1_1
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi

State before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi

State before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply Holds_coincide_Var
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ ∀ (v : VarName),
    isFreeIn v h1_phi → Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d v = Function.updateITE V h1_x d v

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
⊢ ∀ (v : VarName),
    isFreeIn v h1_phi → Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d v = Function.updateITE V h1_x d v
Tactic:
intro x a1
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d x = Function.updateITE V h1_x d x

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d x = Function.updateITE V h1_x d x
Tactic:
simp only [Function.updateITE]
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ (if x = h1_x then d else if x = h1_v then V h1_t else V x) = if x = h1_x then d else V x

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ (if x = h1_x then d else if x = h1_v then V h1_t else V x) = if x = h1_x then d else V x
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝ : x = h1_x
⊢ d = d

case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝¹ : ¬x = h1_x
h✝ : x = h1_v
⊢ V h1_t = V x

case neg
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝¹ : ¬x = h1_x
h✝ : ¬x = h1_v
⊢ V x = V x

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : x = h1_x
⊢ d = d
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : x = h1_v
⊢ V h1_t = V x
Tactic:
case _ c1 c2 =>
  subst c2
  tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : ¬x = h1_v
⊢ V x = V x
Tactic:
case _ c1 c2 =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : x = h1_x
⊢ d = d
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : x = h1_v
⊢ V h1_t = V x
Tactic:
subst c2
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_t : VarName
V : VarAssignment D
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
h1_1 : ¬x = h1_x → ¬isFreeIn x h1_phi
⊢ V h1_t = V x

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_t : VarName
V : VarAssignment D
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
h1_1 : ¬x = h1_x → ¬isFreeIn x h1_phi
⊢ V h1_t = V x
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
c1 : ¬x = h1_x
c2 : ¬x = h1_v
⊢ V x = V x
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : isFreeIn h1_v (exists_ h1_x h1_phi)
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
Tactic:
simp only [isFreeIn] at h1_1
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi'

State before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi'
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'

State before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
specialize h1_ih (Function.updateITE V h1_x d)
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'

State before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
simp only [← h1_ih]
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi

State before:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi
Tactic:
apply Holds_coincide_Var
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ ∀ (v : VarName),
    isFreeIn v h1_phi →
      Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d v =
        Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t) v

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
⊢ ∀ (v : VarName),
    isFreeIn v h1_phi →
      Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d v =
        Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t) v
Tactic:
intro x _
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
⊢ Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d x =
    Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t) x

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
⊢ Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d x =
    Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t) x
Tactic:
simp only [Function.updateITE]
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
⊢ (if x = h1_x then d else if x = h1_v then V h1_t else V x) =
    if x = h1_v then if h1_t = h1_x then d else V h1_t else if x = h1_x then d else V x

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
⊢ (if x = h1_x then d else if x = h1_v then V h1_t else V x) =
    if x = h1_v then if h1_t = h1_x then d else V h1_t else if x = h1_x then d else V x
Tactic:
simp only [eq_comm]
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
⊢ (if h1_x = x then d else if h1_v = x then V h1_t else V x) =
    if h1_v = x then if h1_x = h1_t then d else V h1_t else if h1_x = x then d else V x

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
⊢ (if h1_x = x then d else if h1_v = x then V h1_t else V x) =
    if h1_v = x then if h1_x = h1_t then d else V h1_t else if h1_x = x then d else V x
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
h✝¹ : h1_x = x
h✝ : h1_v = x
⊢ d = V h1_t

case neg
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
h✝¹ : h1_x = x
h✝ : ¬h1_v = x
⊢ d = d

case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
h✝¹ : ¬h1_x = x
h✝ : h1_v = x
⊢ V h1_t = V h1_t

case neg
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
h✝¹ : ¬h1_x = x
h✝ : ¬h1_v = x
⊢ V x = V x

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
c1 : isFreeIn x h1_phi
c2 : h1_x = x
c3 : h1_v = x
⊢ d = V h1_t
Tactic:
case _ c1 c2 c3 =>
  subst c2
  cases h1_1
  case intro h1_1_left h1_1_right =>
    contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
h✝¹ : ¬h1_x = x
h✝ : ¬h1_v = x
⊢ V x = V x
Tactic:
case _ | _ | _ =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi'
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_x a) E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
c1 : isFreeIn x h1_phi
c2 : h1_x = x
c3 : h1_v = x
⊢ d = V h1_t
Tactic:
subst c2
State after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
c1 : isFreeIn h1_x h1_phi
c3 : h1_v = h1_x
⊢ d = V h1_t

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
c1 : isFreeIn h1_x h1_phi
c3 : h1_v = h1_x
⊢ d = V h1_t
Tactic:
cases h1_1
State after:
case intro
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
c1 : isFreeIn h1_x h1_phi
c3 : h1_v = h1_x
left✝ : ¬h1_v = h1_x
right✝ : isFreeIn h1_v h1_phi
⊢ d = V h1_t

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
c1 : isFreeIn h1_x h1_phi
c3 : h1_v = h1_x
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
⊢ d = V h1_t
Tactic:
case intro h1_1_left h1_1_right =>
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
c1 : isFreeIn h1_x h1_phi
c3 : h1_v = h1_x
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
⊢ d = V h1_t
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
h✝¹ : ¬h1_x = x
h✝ : ¬h1_v = x
⊢ V x = V x
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (def_ h1_X h1_xs) ↔
    Holds D I V E (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
induction E
State after:
case nil
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) [] (def_ h1_X h1_xs) ↔
    Holds D I V [] (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

case cons
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tail✝ (def_ h1_X h1_xs) ↔
    Holds D I V tail✝ (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) (head✝ :: tail✝) (def_ h1_X h1_xs) ↔
    Holds D I V (head✝ :: tail✝) (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) [] (def_ h1_X h1_xs) ↔
    Holds D I V [] (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
case nil =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) [] (def_ h1_X h1_xs) ↔
    Holds D I V [] (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) (hd :: tl) (def_ h1_X h1_xs) ↔
    Holds D I V (hd :: tl) (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
⊢ (if h1_X = hd.name ∧ h1_xs.length = hd.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
          (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
        tl hd.q
    else Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs)) ↔
    if h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
        tl hd.q
    else Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
⊢ (if h1_X = hd.name ∧ h1_xs.length = hd.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
          (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
        tl hd.q
    else Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs)) ↔
    if h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
        tl hd.q
    else Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
h✝¹ : h1_X = hd.name ∧ h1_xs.length = hd.args.length
h✝ : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q

case neg
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
h✝¹ : h1_X = hd.name ∧ h1_xs.length = hd.args.length
h✝ : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

case pos
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
h✝¹ : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
h✝ : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q

case neg
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
h✝¹ : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
h✝ : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
case _ c1 c2 =>
  simp only [List.length_map] at c2
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q
Tactic:
case _ c1 c2 =>
  simp at c2
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
case _ c1 c2 =>
  exact ih
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q
Tactic:
simp
State after:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs)) tl hd.q

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs)) tl hd.q
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
          (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v =
        Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v

State before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
          (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v =
        Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v
Tactic:
intro v' a1
State after:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
have s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun (x : VarName) => if h1_v = x then h1_t else x) h1_xs
State after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp only [List.map_eq_map_iff]
State after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
intro x _
State after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp only [Function.updateITE]
State after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if x = h1_v then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if x = h1_v then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp only [eq_comm]
State after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp
State after:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = V (if h1_v = x then h1_t else x)

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case s1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = V (if h1_v = x then h1_t else x)

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
h✝ : h1_v = x
⊢ V h1_t = V h1_t

case neg
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
h✝ : ¬h1_v = x
⊢ V x = V x

case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : h1_v = x
⊢ V h1_t = V h1_t
Tactic:
case _ c3 =>
  simp only [if_pos c3]
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : ¬h1_v = x
⊢ V x = V x
Tactic:
case _ c3 =>
  simp only [if_neg c3]
State after:
no goals

State before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
simp only [s1]
State after:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'

State before:
case h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
      (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs) v'
Tactic:
apply Function.updateListITE_mem_eq_len
State after:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ v' ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs).length

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : h1_v = x
⊢ V h1_t = V h1_t
Tactic:
simp only [if_pos c3]
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a✝ : x ∈ h1_xs
c3 : ¬h1_v = x
⊢ V x = V x
Tactic:
simp only [if_neg c3]
State after:
no goals

State before:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ v' ∈ hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
State after:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args

State before:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args
Tactic:
simp only [← List.mem_toFinset]
State after:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset

State before:
case h1.h1
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset
Tactic:
apply Finset.mem_of_subset hd.h1 a1
State after:
no goals

State before:
case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = (List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs).length
Tactic:
simp
State after:
case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = h1_xs.length

State before:
case h1.h2
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
⊢ hd.args.length = h1_xs.length
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
simp only [List.length_map] at c2
State after:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
c2 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
⊢ Holds D I
      (Function.updateListITE (Function.updateITE V h1_v (V h1_t)) hd.args
        (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs))
      tl hd.q ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q
Tactic:
simp at c2
State after:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : h1_X = hd.name ∧ h1_xs.length = hd.args.length
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)))
      tl hd.q
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
hd : Definition
tl : List Definition
ih :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
c1 : ¬(h1_X = hd.name ∧ h1_xs.length = hd.args.length)
c2 : ¬(h1_X = hd.name ∧ (List.map (fun x => if h1_v = x then h1_t else x) h1_xs).length = hd.args.length)
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) tl (def_ h1_X h1_xs) ↔
    Holds D I V tl (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
exact ih
State after:
no goals