Fixed it to run with metis in the proof loop, which gives a rather minimal set of lemmas. Also got a tactic now, which calls hipspec and automatically does hard induction proofs