simp only [Forall_] at 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
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