As suggested by Pierre-Marie Pédrot in the Coq-club thread:

  [Coq-Club] Very slow failing apply

To work arround some performance issues in Iris.

It is sometimes not desirable to do so.

It no longer requires the functions on both sides of the relation
to be syntactically the same.

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

case H; clear H would fail when H is dependent whereas destruct H
would succeed on that, but just not clear it.

The case tactic is faster than destruct.

Example:

Goal
  ¬False → ¬False → ¬False → ¬False → ¬False → ¬False → ¬False →
  False.
Proof.
  intros. done. (* takes very long *)

Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

In particular, make sure we always try eassumption before reflexivity.

This has bothered me repeatedly in proofs, now I finally got around to fix it at the source

There is still the reals stuff, which is caused by importint Psatz (needed
for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

This is very experimental. It should now deal better with stuff like:

  match x with .. end = match y with .. end

In case there is a hypothesis H : R x y, it will try to destruct it.

Now, for example, when having equiv (Some x) (Some y) it will
try to find a Proper whose range is an equiv before hitting the
eq instance. My hack is general enough that it works for Forall2,
dist, and so on, too.

Contrary to destruct_conj from Program.

It now turns setoid equalities into Leibniz equalities when possible,
and substitutes those.

In principle, we could now un-seal heap_mapsto, saved_prop_own etc., and mark them as "Typeclass Opaque", and ecancel would still work just as fast as it does now.
Thanks to Matthieu for pointing me to this unify feature.