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-p 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.