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
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
no goals