prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
the Judgement Day logs sometimes had entries of the form
at 970:26 (apply):
------------------
------------------
; these were apparently caused by this Mirabelle bug
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
these values were found by Larry in 2007 and using anything else risks losing proofs