Theorem: LN.HoldsClose (FOL/LN/Paper.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
z : String
F : Formula
j : ℕ
h1 : ¬occursIn (free_ z) F
h2 : Formula.lc_at j F
⊢ Holds D I V F ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] F)
Tactic:
induction F generalizing V j
State after:
case pred_
D : Type
I : Interpretation D
z a✝¹ : String
a✝ : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ a✝¹ a✝)
h2 : Formula.lc_at j (pred_ a✝¹ a✝)
⊢ Holds D I V (pred_ a✝¹ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ a✝¹ a✝))

case not_
D : Type
I : Interpretation D
z : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) a✝.not_
h2 : Formula.lc_at j a✝.not_
⊢ Holds D I V a✝.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝.not_)

case imp_
D : Type
I : Interpretation D
z : String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝¹ →
      Formula.lc_at j a✝¹ → (Holds D I V a✝¹ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (a✝¹.imp_ a✝)
h2 : Formula.lc_at j (a✝¹.imp_ a✝)
⊢ Holds D I V (a✝¹.imp_ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
z a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (forall_ a✝¹ a✝)
h2 : Formula.lc_at j (forall_ a✝¹ a✝)
⊢ Holds D I V (forall_ a✝¹ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ a✝¹ a✝))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ X vs)
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
case pred_ X vs =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Formula.openList]
  simp only [Holds]
  congr! 1
  simp
  simp only [List.map_eq_map_iff]
  intro v a1
  specialize h2 v a1
  simp
  cases v
  case _ x =>
    simp only [Var.openList]
    simp only [Var.close]
    have s1 : ¬ free_ x = free_ z
    intro contra
    apply h1
    simp only [← contra]
    exact a1
    simp only [if_neg s1]
  case _ i =>
    simp only [Var.lc_at] at h2
    simp only [Var.openList]
    simp
    split_ifs
    simp only [Var.close]
    simp only [if_pos h2]
State after:
no goals

State before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi.not_
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Holds]
  congr! 1
  exact phi_ih V j h1 h2
State after:
no goals

State before:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (forall_ x phi)
h2 : Formula.lc_at j (forall_ x phi)
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))
Tactic:
case forall_ x phi phi_ih =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Formula.openList]
  simp only [Holds]
  apply forall_congr'
  intro d
  specialize phi_ih (shift D V d) (j + 1) h1 h2
  simp only [phi_ih]
  congr! 1
  apply extracted_1
State after:
no goals

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ X vs)
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
simp only [occursIn] at h1
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
simp only [Formula.lc_at] at h2
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
Tactic:
simp only [Formula.openList]
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (pred_ X (List.map (Var.openList j [free_ z]) vs))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (pred_ X (List.map (Var.openList j [free_ z]) vs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ I.pred_ X (List.map V vs) ↔ I.pred_ X (List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ I.pred_ X (List.map V vs) ↔ I.pred_ X (List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs))
Tactic:
congr! 1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs)

State before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map (V ∘ Var.close j (free_ z)) (List.map (Var.openList j [free_ z]) vs)
Tactic:
simp
State after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) vs

State before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) vs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, V x = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, V x = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) x
Tactic:
intro v a1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v

State before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v
Tactic:
specialize h2 v a1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v

State before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v
Tactic:
simp
State after:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = V (Var.close j (free_ z) (Var.openList j [free_ z] v))

State before:
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = V (Var.close j (free_ z) (Var.openList j [free_ z] v))
Tactic:
cases v
State after:
case a.h.e'_4.free_
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
a✝ : String
a1 : free_ a✝ ∈ vs
h2 : Var.lc_at j (free_ a✝)
⊢ V (free_ a✝) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ a✝)))

case a.h.e'_4.bound_
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
a✝ : ℕ
a1 : bound_ a✝ ∈ vs
h2 : Var.lc_at j (bound_ a✝)
⊢ V (bound_ a✝) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ a✝)))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ x)))
Tactic:
case _ x =>
  simp only [Var.openList]
  simp only [Var.close]
  have s1 : ¬ free_ x = free_ z
  intro contra
  apply h1
  simp only [← contra]
  exact a1
  simp only [if_neg s1]
State after:
no goals

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : Var.lc_at j (bound_ i)
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
Tactic:
case _ i =>
  simp only [Var.lc_at] at h2
  simp only [Var.openList]
  simp
  split_ifs
  simp only [Var.close]
  simp only [if_pos h2]
State after:
no goals

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ x)))
Tactic:
simp only [Var.openList]
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (free_ x))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (free_ x))
Tactic:
simp only [Var.close]
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
have s1 : ¬ free_ x = free_ z
State after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ ¬free_ x = free_ z

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)

State before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ ¬free_ x = free_ z

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
intro contra
State after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ False

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)

State before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ False

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
apply h1
State after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ z ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)

State before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ z ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
simp only [← contra]
State after:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ x ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)

State before:
case s1
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
contra : free_ x = free_ z
⊢ free_ x ∈ vs

D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
exact a1
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
s1 : ¬free_ x = free_ z
⊢ V (free_ x) = V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
simp only [if_neg s1]
State after:
no goals

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : Var.lc_at j (bound_ i)
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
Tactic:
simp only [Var.lc_at] at h2
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
Tactic:
simp only [Var.openList]
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V
      (Var.close j (free_ z)
        (if i < j then bound_ i
        else if x : i - j < [free_ z].length then [free_ z][i - j] else bound_ (i - j - [free_ z].length + j)))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V
      (Var.close j (free_ z)
        (if i < j then bound_ i
        else if x : i - j < [free_ z].length then [free_ z][i - j] else bound_ (i - j - [free_ z].length + j)))
Tactic:
simp
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V (Var.close j (free_ z) (if i < j then bound_ i else if i - j = 0 then free_ z else bound_ (i - j - 1 + j)))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V (Var.close j (free_ z) (if i < j then bound_ i else if i - j = 0 then free_ z else bound_ (i - j - 1 + j)))
Tactic:
split_ifs
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (bound_ i))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (Var.close j (free_ z) (bound_ i))
Tactic:
simp only [Var.close]
State after:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
simp only [if_pos h2]
State after:
no goals

State before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi.not_
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Tactic:
simp only [occursIn] at h1
State after:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)

State before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi.not_
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Tactic:
simp only [Formula.lc_at] at h2
State after:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)

State before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi
⊢ Holds D I V phi.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi.not_)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi
⊢ ¬Holds D I V phi ↔ ¬Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)

State before:
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi
⊢ ¬Holds D I V phi ↔ ¬Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi
⊢ Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
z : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j phi
⊢ Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
Tactic:
exact phi_ih V j h1 h2
State after:
no goals

State before:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (phi.imp_ psi)
h2 : Formula.lc_at j (phi.imp_ psi)
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
simp only [occursIn] at h1
State after:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1 : ¬(occursIn (free_ z) phi ∨ occursIn (free_ z) psi)
h2 : Formula.lc_at j (phi.imp_ psi)
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))

State before:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1 : ¬(occursIn (free_ z) phi ∨ occursIn (free_ z) psi)
h2 : Formula.lc_at j (phi.imp_ psi)
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
push_neg at h1
State after:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j (phi.imp_ psi)
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))

State before:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j (phi.imp_ psi)
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
simp only [Formula.lc_at] at h2
State after:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))

State before:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
left✝ : ¬occursIn (free_ z) phi
right✝ : ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))

State before:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j phi ∧ Formula.lc_at j psi
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
cases h2
State after:
case intro
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
left✝ : Formula.lc_at j phi
right✝ : Formula.lc_at j psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))

State before:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi → Holds D I V psi ↔
    Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi) →
      Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)

State before:
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi → Holds D I V psi ↔
    Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi) →
      Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)
Tactic:
congr! 1
State after:
case a.h.a
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)

case a.h'.a
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
a✝ : Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
⊢ Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)

State before:
case a.h.a
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
⊢ Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
Tactic:
exact phi_ih V j h1_left h2_left
State after:
no goals

State before:
case a.h'.a
D : Type
I : Interpretation D
z : String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1_left : ¬occursIn (free_ z) phi
h1_right : ¬occursIn (free_ z) psi
h2_left : Formula.lc_at j phi
h2_right : Formula.lc_at j psi
a✝ : Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
⊢ Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi)
Tactic:
exact psi_ih V j h1_right h2_right
State after:
no goals

State before:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (forall_ x phi)
h2 : Formula.lc_at j (forall_ x phi)
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))
Tactic:
simp only [occursIn] at h1
State after:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j (forall_ x phi)
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))

State before:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at j (forall_ x phi)
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))
Tactic:
simp only [Formula.lc_at] at h2
State after:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))

State before:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))
Tactic:
simp only [Formula.openList]
State after:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ Holds D I V (forall_ x phi) ↔
    Holds D I (V ∘ Var.close j (free_ z)) (forall_ x (Formula.openList (j + 1) [free_ z] phi))

State before:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ Holds D I V (forall_ x phi) ↔
    Holds D I (V ∘ Var.close j (free_ z)) (forall_ x (Formula.openList (j + 1) [free_ z] phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔
    ∀ (d : D), Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)

State before:
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ (∀ (d : D), Holds D I (shift D V d) phi) ↔
    ∀ (d : D), Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ ∀ (a : D),
    Holds D I (shift D V a) phi ↔
      Holds D I (shift D (V ∘ Var.close j (free_ z)) a) (Formula.openList (j + 1) [free_ z] phi)

State before:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
⊢ ∀ (a : D),
    Holds D I (shift D V a) phi ↔
      Holds D I (shift D (V ∘ Var.close j (free_ z)) a) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)

State before:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
specialize phi_ih (shift D V d) (j + 1) h1 h2
State after:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)

State before:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
simp only [phi_ih]
State after:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi) ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)

State before:
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi) ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
Tactic:
congr! 1
State after:
case h.a.h.e'_3
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ shift D V d ∘ Var.close (j + 1) (free_ z) = shift D (V ∘ Var.close j (free_ z)) d

State before:
case h.a.h.e'_3
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ shift D V d ∘ Var.close (j + 1) (free_ z) = shift D (V ∘ Var.close j (free_ z)) d
Tactic:
apply extracted_1
State after:
no goals