make iApply greatest_fixpoint_paco work in more cases

Discovered by @maxvi: greatest_fixpoint_paco (unlike all the other induction lemmas) had Φ as an implicit parameter, and that eager insertion of the _ could lead to inference failure in cases where leaving it to iApply to insert the _ later would work fine. This fixes the lemma and adds a test.