The testcase is now complete in the sense that the specification for
the justify function explicitly describe the final output list of columns,
while the previous one could be implicitly computed from the synthesized
parameters. It also features a simpler synthesis problem, that should be
the first target to solver.