Some progress on the IL1 proof

It was a little bit broken by the switch to clocked declarations.