beefing up recursion tests with some lemmas about list ops... in progress; tweak to infering instantiation of data constructor type args