Revert "Propagate size info through pattern matching in predicates, for the"

This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea.

Apply again if this kind of dependently typed programming idioms are needed.
Revert "Extend subterm relation to pattern matching in return predicates."

This reverts commit ec1bb8a981fef14b58ab65483244fc42b05aef13.