Theorem: MM0.not_free_imp_is_not_free (FOL/MM0/MM0.lean)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F : Formula
Γ : List (VarName × MetaVarName)
v : VarName
h1 : NotFree Γ v F
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
⊢ IsNotFree D I M E F v
Tactic:
induction F
State after:
case meta_var_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
a✝ : MetaVarName
h1 : NotFree Γ v (meta_var_ a✝)
⊢ IsNotFree D I M E (meta_var_ a✝) v

case pred_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
a✝¹ : PredName
a✝ : List VarName
h1 : NotFree Γ v (pred_ a✝¹ a✝)
⊢ IsNotFree D I M E (pred_ a✝¹ a✝) v

case eq_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
a✝¹ a✝ : VarName
h1 : NotFree Γ v (eq_ a✝¹ a✝)
⊢ IsNotFree D I M E (eq_ a✝¹ a✝) v

case true_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ IsNotFree D I M E true_ v

case not_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
a✝ : Formula
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v a✝.not_
⊢ IsNotFree D I M E a✝.not_ v

case imp_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
a✝¹ a✝ : Formula
a_ih✝¹ : NotFree Γ v a✝¹ → IsNotFree D I M E a✝¹ v
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v (a✝¹.imp_ a✝)
⊢ IsNotFree D I M E (a✝¹.imp_ a✝) v

case forall_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
a✝¹ : VarName
a✝ : Formula
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v (forall_ a✝¹ a✝)
⊢ IsNotFree D I M E (forall_ a✝¹ a✝) v

case def_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
a✝¹ : DefName
a✝ : List VarName
h1 : NotFree Γ v (def_ a✝¹ a✝)
⊢ IsNotFree D I M E (def_ a✝¹ a✝) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : MetaVarName
h1 : NotFree Γ v (meta_var_ X)
⊢ IsNotFree D I M E (meta_var_ X) v
Tactic:
case meta_var_ X =>
  unfold NotFree at h1
  exact h2 X h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : NotFree Γ v (pred_ X xs)
⊢ IsNotFree D I M E (pred_ X xs) v
Tactic:
case pred_ X xs =>
  unfold NotFree at h1
  unfold IsNotFree
  simp only [Holds]
  intro V d
  congr! 1
  apply List.map_congr
  intro x a1
  have s1 : ¬ x = v
  intro contra
  subst contra
  contradiction
  unfold Function.updateITE
  simp only [if_neg s1]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : NotFree Γ v (eq_ x y)
⊢ IsNotFree D I M E (eq_ x y) v
Tactic:
case eq_ x y =>
  unfold NotFree at h1
  unfold IsNotFree
  simp only [Holds]
  intro V d
  cases h1
  case intro h1_left h1_right =>
    simp only [Function.updateITE]
    simp only [if_neg h1_left]
    simp only [if_neg h1_right]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ IsNotFree D I M E true_ v
Tactic:
case true_ =>
  unfold IsNotFree
  intro V d
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi.not_
⊢ IsNotFree D I M E phi.not_ v
Tactic:
case not_ phi phi_ih =>
  unfold NotFree at h1
  unfold IsNotFree at phi_ih
  unfold IsNotFree
  intro V d
  simp only [Holds]
  congr! 1
  exact phi_ih h1 V d
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : MetaVarName
h1 : NotFree Γ v (meta_var_ X)
⊢ IsNotFree D I M E (meta_var_ X) v
Tactic:
unfold NotFree at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : MetaVarName
h1 : (v, X) ∈ Γ
⊢ IsNotFree D I M E (meta_var_ X) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : MetaVarName
h1 : (v, X) ∈ Γ
⊢ IsNotFree D I M E (meta_var_ X) v
Tactic:
exact h2 X h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : NotFree Γ v (pred_ X xs)
⊢ IsNotFree D I M E (pred_ X xs) v
Tactic:
unfold NotFree at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ IsNotFree D I M E (pred_ X xs) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ IsNotFree D I M E (pred_ X xs) v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (pred_ X xs) ↔ Holds D I (Function.updateITE V v d) M E (pred_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (pred_ X xs) ↔ Holds D I (Function.updateITE V v d) M E (pred_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
⊢ ∀ (V : Valuation D) (d : D), I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ I X (List.map V xs) ↔ I X (List.map (Function.updateITE V v d) xs)
Tactic:
congr! 1
State after:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ List.map V xs = List.map (Function.updateITE V v d) xs

State before:
case a.h.e'_2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ List.map V xs = List.map (Function.updateITE V v d) xs
Tactic:
apply List.map_congr
State after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ ∀ x ∈ xs, V x = Function.updateITE V v d x

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
⊢ ∀ x ∈ xs, V x = Function.updateITE V v d x
Tactic:
intro x a1
State after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ V x = Function.updateITE V v d x

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ V x = Function.updateITE V v d x
Tactic:
have s1 : ¬ x = v
State after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ ¬x = v

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x

State before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
⊢ ¬x = v

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
intro contra
State after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
contra : x = v
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x

State before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
contra : x = v
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
subst contra
State after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
X : PredName
xs : List VarName
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
h1 : x ∉ xs
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x

State before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
X : PredName
xs : List VarName
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
h1 : x ∉ xs
⊢ False

case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
contradiction
State after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = Function.updateITE V v d x
Tactic:
unfold Function.updateITE
State after:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = if x = v then d else V x

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : v ∉ xs
V : Valuation D
d : D
x : VarName
a1 : x ∈ xs
s1 : ¬x = v
⊢ V x = if x = v then d else V x
Tactic:
simp only [if_neg s1]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : NotFree Γ v (eq_ x y)
⊢ IsNotFree D I M E (eq_ x y) v
Tactic:
unfold NotFree at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ IsNotFree D I M E (eq_ x y) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ IsNotFree D I M E (eq_ x y) v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (eq_ x y) ↔ Holds D I (Function.updateITE V v d) M E (eq_ x y)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (eq_ x y) ↔ Holds D I (Function.updateITE V v d) M E (eq_ x y)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
⊢ ∀ (V : Valuation D) (d : D), V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
V : Valuation D
d : D
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
h1 : ¬x = v ∧ ¬y = v
V : Valuation D
d : D
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
left✝ : ¬x = v
right✝ : ¬y = v
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
case intro h1_left h1_right =>
  simp only [Function.updateITE]
  simp only [if_neg h1_left]
  simp only [if_neg h1_right]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ Function.updateITE V v d x = Function.updateITE V v d y
Tactic:
simp only [Function.updateITE]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ (if x = v then d else V x) = if y = v then d else V y

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ (if x = v then d else V x) = if y = v then d else V y
Tactic:
simp only [if_neg h1_left]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ V x = if y = v then d else V y

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x y : VarName
V : Valuation D
d : D
h1_left : ¬x = v
h1_right : ¬y = v
⊢ V x = V y ↔ V x = if y = v then d else V y
Tactic:
simp only [if_neg h1_right]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ IsNotFree D I M E true_ v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
V : Valuation D
d : D
⊢ Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
h1 : NotFree Γ v true_
V : Valuation D
d : D
⊢ Holds D I V M E true_ ↔ Holds D I (Function.updateITE V v d) M E true_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi.not_
⊢ IsNotFree D I M E phi.not_ v
Tactic:
unfold NotFree at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v
Tactic:
unfold IsNotFree at phi_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ IsNotFree D I M E phi.not_ v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi.not_ ↔ Holds D I (Function.updateITE V v d) M E phi.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ ¬Holds D I V M E phi ↔ ¬Holds D I (Function.updateITE V v d) M E phi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ ¬Holds D I V M E phi ↔ ¬Holds D I (Function.updateITE V v d) M E phi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
Tactic:
exact phi_ih h1 V d
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v (phi.imp_ psi)
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold NotFree at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold IsNotFree at phi_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold IsNotFree at psi_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E (phi.imp_ psi) ↔ Holds D I (Function.updateITE V v d) M E (phi.imp_ psi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
V : Valuation D
d : D
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
psi_ih :
  NotFree Γ v psi → ∀ (V : Valuation D) (d : D), Holds D I V M E psi ↔ Holds D I (Function.updateITE V v d) M E psi
V : Valuation D
d : D
left✝ : NotFree Γ v phi
right✝ : NotFree Γ v psi
⊢ Holds D I V M E phi → Holds D I V M E psi ↔
    Holds D I (Function.updateITE V v d) M E phi → Holds D I (Function.updateITE V v d) M E psi

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

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

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

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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : NotFree Γ v (forall_ x phi)
⊢ IsNotFree D I M E (forall_ x phi) v
Tactic:
unfold NotFree at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v
Tactic:
unfold IsNotFree at phi_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ IsNotFree D I M E (forall_ x phi) v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ Holds D I V M E (forall_ x phi) ↔ Holds D I (Function.updateITE V v d) M E (forall_ x phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M E phi) ↔
    ∀ (d_1 : D), Holds D I (Function.updateITE (Function.updateITE V v d) x d_1) M E phi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M E phi) ↔
    ∀ (d_1 : D), Holds D I (Function.updateITE (Function.updateITE V v d) x d_1) M E phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x a) M E phi

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d : D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x a) M E phi
Tactic:
intro d'
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
by_cases c1 : x = v
State after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
c1 : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi

case neg
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
c1 : ¬x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi

State before:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
c1 : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
cases h1
State after:
case pos.inl
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 h✝ : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi

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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 c2 : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
case _ c2 =>
  subst c1
  simp only [Function.updateITE_idem]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
case _ c2 =>
  subst c1
  simp only [Function.updateITE_idem]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 c2 : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
subst c1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : x = x
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x d') M E phi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : x = x
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x d') M E phi
Tactic:
simp only [Function.updateITE_idem]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
subst c1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : NotFree Γ x phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x d') M E phi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
V : Valuation D
d d' : D
h2 : ∀ (X : MetaVarName), (x, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) x
phi_ih :
  NotFree Γ x phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V x d) M E phi
c2 : NotFree Γ x phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d) x d') M E phi
Tactic:
simp only [Function.updateITE_idem]
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
h1 : x = v ∨ NotFree Γ v phi
V : Valuation D
d d' : D
c1 : ¬x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
cases h1
State after:
case neg.inl
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
h✝ : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi

case neg.inr
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
h✝ : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
case _ c2 =>
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
case _ c2 =>
  simp only [← Function.updateITE_comm V x v d d' c1]
  exact phi_ih c2 (Function.updateITE V x d') d
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : x = v
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V v d) x d') M E phi
Tactic:
simp only [← Function.updateITE_comm V x v d d' c1]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d') v d) M E phi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
x : VarName
phi : Formula
phi_ih :
  NotFree Γ v phi → ∀ (V : Valuation D) (d : D), Holds D I V M E phi ↔ Holds D I (Function.updateITE V v d) M E phi
V : Valuation D
d d' : D
c1 : ¬x = v
c2 : NotFree Γ v phi
⊢ Holds D I (Function.updateITE V x d') M E phi ↔ Holds D I (Function.updateITE (Function.updateITE V x d') v d) M E phi
Tactic:
exact phi_ih c2 (Function.updateITE V x d') d
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
⊢ IsNotFree D I M E (def_ X xs) v
Tactic:
induction E
State after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ IsNotFree D I M [] (def_ X xs) v

case cons
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M tail✝ (meta_var_ X) v) → IsNotFree D I M tail✝ (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (head✝ :: tail✝) (meta_var_ X) v
⊢ IsNotFree D I M (head✝ :: tail✝) (def_ X xs) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ IsNotFree D I M [] (def_ X xs) v
Tactic:
case nil =>
  unfold IsNotFree
  intro V d
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ IsNotFree D I M [] (def_ X xs) v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ ∀ (V : Valuation D) (d : D), Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
V : Valuation D
d : D
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
V : Valuation D
d : D
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M [] (def_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold NotFree at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold IsNotFree at h2
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 :
  ∀ (X : MetaVarName),
    (v, X) ∈ Γ →
      ∀ (V : Valuation D) (d : D),
        Holds D I V M (E_hd :: E_tl) (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (meta_var_ X)
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 :
  ∀ (X : MetaVarName),
    (v, X) ∈ Γ →
      ∀ (V : Valuation D) (d : D),
        Holds D I V M (E_hd :: E_tl) (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (meta_var_ X)
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
simp only [Holds] at h2
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold IsNotFree at E_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  (∀ (X : MetaVarName),
      (v, X) ∈ Γ →
        ∀ (V : Valuation D) (d : D),
          Holds D I V M E_tl (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M E_tl (meta_var_ X)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih :
  (∀ (X : MetaVarName),
      (v, X) ∈ Γ →
        ∀ (V : Valuation D) (d : D),
          Holds D I V M E_tl (meta_var_ X) ↔ Holds D I (Function.updateITE V v d) M E_tl (meta_var_ X)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
simp only [Holds] at E_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
Tactic:
unfold IsNotFree
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M (E_hd :: E_tl) (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    Holds D I V M (E_hd :: E_tl) (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    (if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
      else Holds D I V M E_tl (def_ X xs)) ↔
      if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE (Function.updateITE V v d) E_hd.args (List.map (Function.updateITE V v d) xs))
          M E_tl E_hd.F
      else Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
⊢ ∀ (V : Valuation D) (d : D),
    (if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
      else Holds D I V M E_tl (def_ X xs)) ↔
      if X = E_hd.name ∧ xs.length = E_hd.args.length then
        Holds D I (Function.updateListITE (Function.updateITE V v d) E_hd.args (List.map (Function.updateITE V v d) xs))
          M E_tl E_hd.F
      else Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
Tactic:
intro V a
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
        E_tl E_hd.F
    else Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
        E_tl E_hd.F
    else Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
      E_tl E_hd.F

case neg
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Tactic:
case _ c1 =>
  exact E_ih h2 V a
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map V xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M
      E_tl E_hd.F
Tactic:
apply holds_coincide_var D I (Function.updateListITE V E_hd.args (List.map V xs)) (Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs)) M E_tl E_hd.F E_hd.args E_hd.nf
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ v_1 ∈ E_hd.args,
    Function.updateListITE V E_hd.args (List.map V xs) v_1 =
      Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v_1

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ v_1 ∈ E_hd.args,
    Function.updateListITE V E_hd.args (List.map V xs) v_1 =
      Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v_1
Tactic:
intro v' a1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ Function.updateListITE V E_hd.args (List.map V xs) v' =
    Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v'

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ Function.updateListITE V E_hd.args (List.map V xs) v' =
    Function.updateListITE (Function.updateITE V v a) E_hd.args (List.map (Function.updateITE V v a) xs) v'
Tactic:
apply Function.updateListITE_map_updateIte V (Function.updateITE V v a)
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ ∀ y ∈ xs, ¬y = v

case h2
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ E_hd.args.length = xs.length

case h3
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ v' ∈ E_hd.args

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ ∀ y ∈ xs, ¬y = v
Tactic:
intro y a2 contra
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
contra : y = v
⊢ False

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
contra : y = v
⊢ False
Tactic:
subst contra
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
h1 : y ∉ xs
h2 : ∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)
E_ih :
  (∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V y d) M E_tl (def_ X xs)
⊢ False

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
y : VarName
a2 : y ∈ xs
h1 : y ∉ xs
h2 : ∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)
E_ih :
  (∀ (X : MetaVarName), (y, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V y d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V y d) M E_tl (def_ X xs)
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ E_hd.args.length = xs.length
Tactic:
cases c1
State after:
case h2.intro
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
v' : VarName
a1 : v' ∈ E_hd.args
left✝ : X = E_hd.name
right✝ : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
v' : VarName
a1 : v' ∈ E_hd.args
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
case intro c1_left c1_right =>
simp only [c1_right]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
v' : VarName
a1 : v' ∈ E_hd.args
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
simp only [c1_right]
State after:
no goals

State before:
case h3
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v' : VarName
a1 : v' ∈ E_hd.args
⊢ v' ∈ E_hd.args
Tactic:
exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
h1 : v ∉ xs
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)
E_ih :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → ∀ (V : Valuation D) (d : D), M X V ↔ M X (Function.updateITE V v d)) →
    ∀ (V : Valuation D) (d : D),
      Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v d) M E_tl (def_ X xs)
V : Valuation D
a : D
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I (Function.updateITE V v a) M E_tl (def_ X xs)
Tactic:
exact E_ih h2 V a
State after:
no goals