That way, we can use Contractive as part of structure definitions in
which we do not have a bundled OFE yet.

Now, we never need to unfold LimitPreserving in LambdaRust, and hence
the entails_lim tactic is no longer needed.

Also, give names to hypotheses that we refer to.

Also add "Local" to some Default Proof Using to keep them more contained

This approach is originally by Robbert

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing