Un-reduced type constructor variables

[alexfmpe]

While a -> a and (a -> b) -> [a] -> [b] have their relation variables reduced into functions, that's not the case for (forall x. a x -> a x) and (a -> b) -> f a -> f b, so we don't end up without a equal/inequal theorem.

The problem is that unfoldFormula simply returns return . Predicate . IsMember x y $ rel for RelConsFunVar (with #3) and RelTypeConsApp. I'm not sufficiently familiar with free theorem derivation to know what they should return instead though.