case cons xs_hd xs_tl xs_ih =>
  simp only [Forall_]
  apply deduction_theorem
  simp
  apply IsDeduct.mp_ (Forall_ xs_tl P)
  apply proof_imp_deduct
  exact xs_ih
  apply specId xs_hd
  apply IsDeduct.assume_
  simp
  rfl
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ (xs_hd :: xs_tl) P).imp_ P)
no goals