Changes:
  - proofs now once again have lists, instead of k-vectors, of
  arguments, as this was easier to integrate with agda's reflection