Prove a theorem using FGL with case-splitting.

The usage of

:param-bindings is the same as in ACL2::def-gl-param-thm, but the shape specifier alist in each entry is ignored.:param-hyp is the same as in ACL2::def-gl-param-thm.:split-params provides the fgl-sat-check parameters object for proving that case split provided covers all cases.:solve-params provides the fgl-sat-check object for proving each case.:repeat-concl controls whether the conclusion is (if nil) rewritten/symbolically executed once and then solved separately for each case, or (if nonnil) rewritten/symbolically executed (and also solved) separately for each case.:hints gives a list of hints (computed or subgoal) that are provided before the casesplit and FGL interpreter clause processor hints. Practically speaking, if these hints don't trigger immediately, then they won't trigger until after the casesplit and FGL interpreter hints, since those occur unconditionally.:split-concl pertains to cases where previous hints have allowed ACL2 to clausify the conjecture -- normally, the case split happens on the original, unclausified conjecture. If:split-concl is non-nil (the default), then the last literal in the clause is considered the conclusion and previous literals are bundled into the hypothesis; if nil, then the whole clause is bundled into the conclusion and the hyp is just T.