Theorem: FOL.NV.Forall_spec_id' (FOL/NV/Margaris/Fol.lean)

State before:
xs : List VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ xs P)
⊢ IsDeduct Δ P
Tactic:
induction xs
State after:
case nil
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ [] P)
⊢ IsDeduct Δ P

case cons
P : Formula
Δ : Set Formula
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsDeduct Δ (Forall_ tail✝ P) → IsDeduct Δ P
h1 : IsDeduct Δ (Forall_ (head✝ :: tail✝) P)
⊢ IsDeduct Δ P

State before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ [] P)
⊢ IsDeduct Δ P
Tactic:
case nil =>
  simp only [Forall_] at h1
  simp at h1
  exact h1
State after:
no goals

State before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (Forall_ (xs_hd :: xs_tl) P)
⊢ IsDeduct Δ P
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp only [Forall_] at h1
  simp at h1
  apply xs_ih
  simp only [Forall_]
  apply specId xs_hd
  exact h1
State after:
no goals

State before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (Forall_ [] P)
⊢ IsDeduct Δ P
Tactic:
simp only [Forall_] at h1
State after:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (List.foldr forall_ P [])
⊢ IsDeduct Δ P

State before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (List.foldr forall_ P [])
⊢ IsDeduct Δ P
Tactic:
simp at h1
State after:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P

State before:
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Tactic:
exact h1
State after:
no goals

State before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (Forall_ (xs_hd :: xs_tl) P)
⊢ IsDeduct Δ P
Tactic:
simp only [Forall_] at h1
State after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (List.foldr forall_ P (xs_hd :: xs_tl))
⊢ IsDeduct Δ P

State before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (List.foldr forall_ P (xs_hd :: xs_tl))
⊢ IsDeduct Δ P
Tactic:
simp at h1
State after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ P

State before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ P
Tactic:
apply xs_ih
State after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (Forall_ xs_tl P)

State before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (Forall_ xs_tl P)
Tactic:
simp only [Forall_]
State after:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (List.foldr forall_ P xs_tl)

State before:
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (List.foldr forall_ P xs_tl)
Tactic:
apply specId xs_hd
State after:
case h1
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))

State before:
case h1
P : Formula
Δ : Set Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsDeduct Δ (Forall_ xs_tl P) → IsDeduct Δ P
h1 : IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
⊢ IsDeduct Δ (forall_ xs_hd (List.foldr forall_ P xs_tl))
Tactic:
exact h1
State after:
no goals