Fix a syntax error
Try to admit everything at once

Since coq cycles are expensive in comparison with python cycles, we now
first try to admit everything at once.