apply IsDeduct.assume_
case h1.a.h1
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_hd (Forall_ xs_tl P))
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ forall_ xs_hd (Forall_ xs_tl P) ∈ {forall_ xs_hd (List.foldr forall_ P xs_tl)}