apply xs_ih
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
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)