exact xs_ih
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ xs_tl P).imp_ P)

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