[Parametric] reduce instantiation cycles

             * produce only new instances
             * don't cycle on polymorphic lemma without binder
               length nil = 0