letgetExpandingFunctionProducerfunc=oval(obind(obind(List.assoc_optfuncimplementationLookup)(funimpl->These.fstimpl))getTableau)(fun_->raise(CoAlgFormula.CoAlgException("one-step tableau based satisfiability is not implemented for "^string_of_functorfunc)))
letoneStepSatisfiabilityfunc=oval(obind(obind(List.assoc_optfuncimplementationLookup)(funimpl->These.sndimpl))getOneStepFun)(fun_->raise(CoAlgFormula.CoAlgException("one-step function based satisfiability is not implemented for "^string_of_functorfunc)))
letgetExpandingFunctionProducerfunc=oval(obind(List.assoc_optfuncimplementationLookup)getTableau)(fun_->raise(CoAlgFormula.CoAlgException("one-step tableau based satisfiability is not implemented for "^string_of_functorfunc)))
letoneStepSatisfiabilityfunc=oval(obind(List.assoc_optfuncimplementationLookup)getOneStepFun)(fun_->raise(CoAlgFormula.CoAlgException("one-step function based satisfiability is not implemented for "^string_of_functorfunc)))