termination checking for deep pattern matches

Stream: lean4

[Jad Ghalayini]

Termination checking doesn't seem to work for deep pattern matches, which makes it impossible to write recursive functions for inductive types having, e.g., recursive products as constructor parameters. See my issue @ https://github.com/leanprover/lean4/issues/770