I should have added that it's clear that there
could be a problem if `
A` were instantiated with `
t`, but I haven't instantiated it yet. Couldn't the error message be invoked only when I try to instantiate `
A` to `
t`, which I would generally avoid, instead of being invoked if I use any subordination in my development at all? Going even further, what's actually wrong with `
member_prune[t]`? Under the subordination declaration, this theorem should be vacuously true, since the only `
E` that it could be applied to would already be a constant function. (Yes, I know that polymorphic theorems need parametric proofs, but ...)