induction xs
xs : List VarName
P : Formula
⊢ IsProof ((Forall_ xs P).imp_ P)
case nil
P : Formula
⊢ IsProof ((Forall_ [] P).imp_ P)

case cons
P : Formula
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsProof ((Forall_ tail✝ P).imp_ P)
⊢ IsProof ((Forall_ (head✝ :: tail✝) P).imp_ P)