Attempt at better Abbrev protection

This in the face of simplification and the variable elimination done
by RW_TAC and friends. Core sequence, -t1 and some of -t2 builds (up
to category theory example).

Machinery for dynamically reverting to the old behaviours possible
through diminish_srw_ss and a trace variable.

This is work on github issue #800

Fix proofs broken by 508f79ea974

Prove unary recursive functions are equivalent to n-ary ones

Inspired by Mario Carneiro's paper at ITP this year.