Add theorem list validation to goal

Because goal has type '(string * Protected<thm0>) list * term',
erroneous theorems could be passed into the list.

We add
let! _ = Choice.List.map snd asl
so that if the list consists of an exception, the exception will be
returned immediately.

It will prevent a goalstate to be successful although it will produce an
exception.

Limit 10 steps in ITAUT_TAC (the OCaml version only needs up to 5 steps
to prove theorems).

Currently there are 70 failing theorems.
Use Choice.List.fold instead of rev_itlist

When an exception is created, Choice.List.fold will return immediately
but rev_itlist will not