My one comment here is that I think it would be better to only create one Lemma the registers for all the tests and run each of the tests on that lemma instead of running them each individually.