Theorem: keepFreshH (Pdl/Unfold.lean)

State before:
x : ℕ
α : Program
⊢ x ∉ voc α → ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
Tactic:
intro x_notin F δ Fδ_in_H
State after:
x : ℕ
α : Program
x_notin : x ∉ voc α
F : List Formula
δ : List Program
Fδ_in_H : (F, δ) ∈ H α
⊢ x ∉ voc F ∧ x ∉ voc δ

State before:
x : ℕ
α : Program
x_notin : x ∉ voc α
F : List Formula
δ : List Program
Fδ_in_H : (F, δ) ∈ H α
⊢ x ∉ voc F ∧ x ∉ voc δ
Tactic:
cases α
State after:
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : x ∉ voc (·a✝)
Fδ_in_H : (F, δ) ∈ H (·a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹;'a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹;'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹⋓a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹⋓a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ voc (∗a✝)
Fδ_in_H : (F, δ) ∈ H (∗a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

State before:
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : x ∉ voc (·a✝)
Fδ_in_H : (F, δ) ∈ H (·a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹;'a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹;'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹⋓a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹⋓a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ voc (∗a✝)
Fδ_in_H : (F, δ) ∈ H (∗a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ
Tactic:
all_goals
  simp [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram] at *
State after:
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : ¬x = a✝
Fδ_in_H : F = [] ∧ δ = [·a✝]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

State before:
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
Fδ_in_H : F = [] ∧ δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
case atom_prog a =>
  cases Fδ_in_H
  subst_eqs
  simp [vocabOfProgram]
  assumption
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
case test =>
  cases Fδ_in_H
  subst_eqs
  aesop
State after:
no goals

State before:
case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
all_goals
  constructor <;> intro y y_in
State after:
case sequence.left
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case sequence.right
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

case union.left
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case union.right
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

case star.left
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case star.right
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

State before:
case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ
Tactic:
simp [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram] at *
State after:
case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

State before:
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
Fδ_in_H : F = [] ∧ δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
cases Fδ_in_H
State after:
case intro
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
left✝ : F = []
right✝ : δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

State before:
case intro
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
left✝ : F = []
right✝ : δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
subst_eqs
State after:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ (∀ x_1 ∈ [], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [·a], x ∉ vocabOfProgram x_1

State before:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ (∀ x_1 ∈ [], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [·a], x ∉ vocabOfProgram x_1
Tactic:
simp [vocabOfProgram]
State after:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ ¬x = a

State before:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ ¬x = a
Tactic:
assumption
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
cases Fδ_in_H
State after:
case intro
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
left✝ : F = [a✝]
right✝ : δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

State before:
case intro
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
left✝ : F = [a✝]
right✝ : δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
subst_eqs
State after:
case intro.refl.refl
x : ℕ
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
⊢ (∀ x_1 ∈ [a✝], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [], x ∉ vocabOfProgram x_1

State before:
case intro.refl.refl
x : ℕ
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
⊢ (∀ x_1 ∈ [a✝], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [], x ∉ vocabOfProgram x_1
Tactic:
aesop
State after:
no goals

State before:
case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
constructor <;> intro y y_in
State after:
case star.left
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case star.right
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

State before:
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
Tactic:
rcases Fδ_in_H with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in, def_l⟩⟩, Fδ_in_l⟩⟩
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
def_l : (if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]) = l
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
def_l : (if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]) = l
⊢ x ∉ vocabOfFormula y
Tactic:
subst def_l
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]
⊢ x ∉ vocabOfFormula y
Tactic:
cases em (δ' = []) <;> simp_all
State after:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
h✝ : δ' = []
⊢ x ∉ vocabOfFormula y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' : List Formula
δ' : List Program
y_in : y ∈ F'
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
h✝ : δ' = []
⊢ x ∉ vocabOfFormula y
Tactic:
subst_eqs
State after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Tactic:
have IHα := keepFreshH α x_notin.1 F' [] Fδ'_in
State after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : x ∉ voc F' ∧ x ∉ voc []
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : x ∉ voc F' ∧ x ∉ voc []
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula y
Tactic:
rcases Fδ_in_l with ⟨l', ⟨⟨a', b', ⟨a'b'_in_Hβ, def_l'⟩⟩, Fδ_in_l'⟩⟩
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
l' : List (List Formula × List Program)
Fδ_in_l' : (F, δ) ∈ l'
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
def_l' : [(F' ∪ a', b')] = l'
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
l' : List (List Formula × List Program)
Fδ_in_l' : (F, δ) ∈ l'
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
def_l' : [(F' ∪ a', b')] = l'
⊢ x ∉ vocabOfFormula y
Tactic:
subst_eqs
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : (F, δ) ∈ [(F' ∪ a', b')]
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : (F, δ) ∈ [(F' ∪ a', b')]
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
y_in : y ∈ F' ∨ y ∈ a'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
y_in : y ∈ F' ∨ y ∈ a'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
⊢ x ∉ vocabOfFormula y
Tactic:
cases y_in
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ x ∉ vocabOfFormula y

case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ x ∉ vocabOfFormula y
Tactic:
apply IHα
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl.a
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ y ∈ F'

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl.a
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ y ∈ F'
Tactic:
assumption
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
⊢ x ∉ vocabOfFormula y
Tactic:
have IHβ := keepFreshH β x_notin.2 a' b' a'b'_in_Hβ
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' : List Formula
δ' : List Program
y_in : y ∈ F'
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfFormula y
Tactic:
have := keepFreshH α x_notin.1 F' δ' Fδ'_in
State after:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' : List Formula
δ' : List Program
y_in : y ∈ F'
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
this : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' : List Formula
δ' : List Program
y_in : y ∈ F'
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
this : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y
Tactic:
rcases Fδ_in_H with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in, def_l⟩⟩, Fδ_in_l⟩⟩
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
def_l : (if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]) = l
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
def_l : (if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]) = l
⊢ x ∉ vocabOfProgram y
Tactic:
subst def_l
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]
⊢ x ∉ vocabOfProgram y
Tactic:
cases em (δ' = []) <;> simp_all
State after:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = β
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
State after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram y
Tactic:
have IHα := keepFreshH α x_notin.1 F' [] Fδ'_in
State after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : x ∉ voc F' ∧ x ∉ voc []
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : x ∉ voc F' ∧ x ∉ voc []
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfProgram y
Tactic:
rcases Fδ_in_l with ⟨l', ⟨⟨a', b', ⟨a'b'_in_Hβ, def_l'⟩⟩, Fδ_in_l'⟩⟩
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
l' : List (List Formula × List Program)
Fδ_in_l' : (F, δ) ∈ l'
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
def_l' : [(F' ∪ a', b')] = l'
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
l' : List (List Formula × List Program)
Fδ_in_l' : (F, δ) ∈ l'
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
def_l' : [(F' ∪ a', b')] = l'
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : (F, δ) ∈ [(F' ∪ a', b')]
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : (F, δ) ∈ [(F' ∪ a', b')]
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
⊢ x ∉ vocabOfProgram y
Tactic:
have IHβ := keepFreshH β x_notin.2 a' b' a'b'_in_Hβ
State after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = β
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
cases y_in
State after:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y = β
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y
Tactic:
have IHα := keepFreshH α x_notin.1 F' δ' Fδ'_in
State after:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y = β
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
State after:
case intro.intro.intro.intro.intro.inr.inr.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram β

State before:
case intro.intro.intro.intro.intro.inr.inr.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram β
Tactic:
tauto
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H : (F, δ) ∈ H α ∨ (F, δ) ∈ H β
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
Tactic:
cases Fδ_in_H
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfFormula y

case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfFormula y

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfFormula y
Tactic:
have IHα := keepFreshH α x_notin.1 F δ
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfFormula y
Tactic:
have IHβ := keepFreshH β x_notin.2 F δ
State after:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y

State before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H : (F, δ) ∈ H α ∨ (F, δ) ∈ H β
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y
Tactic:
cases Fδ_in_H
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfProgram y

case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfProgram y

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfProgram y
Tactic:
have IHα := keepFreshH α x_notin.1 F δ
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfProgram y
Tactic:
have IHβ := keepFreshH β x_notin.2 F δ
State after:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y

State before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
Tactic:
cases Fδ_in_H
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfFormula y

case inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y

State before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
hyp : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Tactic:
case inr hyp =>
  rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, def_l⟩⟩, Fδ_in_l⟩⟩
  subst def_l
  have IHα := keepFreshH α x_notin F' δ' Fδ'_in_Hα
  cases em (δ' = []) <;> simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfFormula y
Tactic:
exfalso
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ False

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ False
Tactic:
simp_all
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
hyp : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Tactic:
rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, def_l⟩⟩, Fδ_in_l⟩⟩
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] else [(F', δ' ++ [∗α])]) = l
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] else [(F', δ' ++ [∗α])]) = l
⊢ x ∉ vocabOfFormula y
Tactic:
subst def_l
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
⊢ x ∉ vocabOfFormula y
Tactic:
have IHα := keepFreshH α x_notin F' δ' Fδ'_in_Hα
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfFormula y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfFormula y
Tactic:
cases em (δ' = []) <;> simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y
Tactic:
cases Fδ_in_H
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfProgram y

case inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram y

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfProgram y
Tactic:
exfalso
State after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ False

State before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ False
Tactic:
simp_all
State after:
no goals

State before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
hyp : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram y
Tactic:
rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, def_l⟩⟩, Fδ_in_l⟩⟩
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] else [(F', δ' ++ [∗α])]) = l
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] else [(F', δ' ++ [∗α])]) = l
⊢ x ∉ vocabOfProgram y
Tactic:
subst def_l
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
⊢ x ∉ vocabOfProgram y
Tactic:
have IHα := keepFreshH α x_notin F' δ' Fδ'_in_Hα
State after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Tactic:
cases em (δ' = [])
State after:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [∗α]
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [∗α]
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
cases Fδ_in_l
State after:
case intro.intro.intro.intro.intro.inr.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
left✝ : F = F'
right✝ : δ = δ' ++ [∗α]
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inr.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
left✝ : F = F'
right✝ : δ = δ' ++ [∗α]
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
State after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram y
Tactic:
cases y_in
State after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y = (∗α)
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y
Tactic:
have := keepFreshH α x_notin F δ' Fδ'_in_Hα
State after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
this : x ∉ voc F ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y

State before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
this : x ∉ voc F ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y = (∗α)
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
State after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram (∗α)

State before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram (∗α)
Tactic:
simp [vocabOfProgram]
State after:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram α

State before:
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inr.refl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
δ' : List Program
h✝ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram α
Tactic:
exact x_notin
State after:
no goals