Program: refine shrinking of obligations

Ensure correspondence between the term and type to shrink, so that Lets
are preserved when they are used relevantly in either of them.  This
avoids e.g. "simpl" in the shrinked hypotheses to reduce shrinking,
while maintaining unsimplified types in the type of the shrinked
obligations (for compatibility).
Simplify Lambda, Prod case of shrinking,
By invariant (we start with a term and its type), the abstraction's
types correspond.

0 files changed, 0 insertions, 0 deletions