Theorem: vocOfBigDis (Bml/bigConDis.lean)

State before:
x : Char
l : List Formula
⊢ x ∈ voc (bigDis l) → ∃ φ ∈ l, x ∈ voc φ
Tactic:
intro hyp
State after:
x : Char
l : List Formula
hyp : x ∈ voc (bigDis l)
⊢ ∃ φ ∈ l, x ∈ voc φ

State before:
x : Char
l : List Formula
hyp : x ∈ voc (bigDis l)
⊢ ∃ φ ∈ l, x ∈ voc φ
Tactic:
induction l
State after:
case nil
x : Char
hyp : x ∈ voc (bigDis [])
⊢ ∃ φ ∈ [], x ∈ voc φ

case cons
x : Char
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : x ∈ voc (bigDis tail✝) → ∃ φ ∈ tail✝, x ∈ voc φ
hyp : x ∈ voc (bigDis (head✝ :: tail✝))
⊢ ∃ φ ∈ head✝ :: tail✝, x ∈ voc φ

State before:
x : Char
hyp : x ∈ voc (bigDis [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
case nil  => aesop
State after:
no goals

State before:
x : Char
hyp : x ∈ voc (bigDis [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
aesop
State after:
no goals

State before:
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
cases em (x ∈ vocabOfFormula head)
State after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

State before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
simp
State after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a

State before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a
Tactic:
tauto
State after:
no goals

State before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
unfold bigDis at hyp
State after:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

State before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
aesop
State after:
no goals