simp only [Forall_]
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ (xs_hd :: xs_tl) P).imp_ P)
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)