apply deduction_theorem
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((List.foldr forall_ P (xs_hd :: xs_tl)).imp_ P)
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct (∅ ∪ {List.foldr forall_ P (xs_hd :: xs_tl)}) P