Theorem: FOL.NV.Forall_isBoundIn (FOL/NV/Margaris/Fol.lean)

State before:
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (Forall_ xs P) ↔ x ∈ xs ∨ isBoundIn x P
Tactic:
simp only [Formula.Forall_]
State after:
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (List.foldr forall_ P xs) ↔ x ∈ xs ∨ isBoundIn x P

State before:
P : Formula
xs : List VarName
x : VarName
⊢ isBoundIn x (List.foldr forall_ P xs) ↔ x ∈ xs ∨ isBoundIn x P
Tactic:
induction xs
State after:
case nil
P : Formula
x : VarName
⊢ isBoundIn x (List.foldr forall_ P []) ↔ x ∈ [] ∨ isBoundIn x P

case cons
P : Formula
x head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isBoundIn x (List.foldr forall_ P tail✝) ↔ x ∈ tail✝ ∨ isBoundIn x P
⊢ isBoundIn x (List.foldr forall_ P (head✝ :: tail✝)) ↔ x ∈ head✝ :: tail✝ ∨ isBoundIn x P

State before:
P : Formula
x : VarName
⊢ isBoundIn x (List.foldr forall_ P []) ↔ x ∈ [] ∨ isBoundIn x P
Tactic:
case nil =>
  simp
State after:
no goals

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∈ xs_hd :: xs_tl ∨ isBoundIn x P
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp
  simp only [isBoundIn]
  simp only [xs_ih]
  tauto
State after:
no goals

State before:
P : Formula
x : VarName
⊢ isBoundIn x (List.foldr forall_ P []) ↔ x ∈ [] ∨ isBoundIn x P
Tactic:
simp
State after:
no goals

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∈ xs_hd :: xs_tl ∨ isBoundIn x P
Tactic:
simp
State after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ isBoundIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Tactic:
simp only [isBoundIn]
State after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ isBoundIn x (List.foldr forall_ P xs_tl) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ isBoundIn x (List.foldr forall_ P xs_tl) ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Tactic:
simp only [xs_ih]
State after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ x ∈ xs_tl ∨ isBoundIn x P ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isBoundIn x (List.foldr forall_ P xs_tl) ↔ x ∈ xs_tl ∨ isBoundIn x P
⊢ x = xs_hd ∨ x ∈ xs_tl ∨ isBoundIn x P ↔ (x = xs_hd ∨ x ∈ xs_tl) ∨ isBoundIn x P
Tactic:
tauto
State after:
no goals