new todo, improved error message, better typesetting of variants in

inductive proofs.
Fixed line numbers in the parser.
o Added an implication rule.
o Added a function theorem to deal with (f | x0 → y).x1
o Added an example of phase synchronisation algorithm
o Made a variant of the cubes example where we keep producing cubes
without limits
o