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.

This is more consistent with the proofmode, where we also call it pure.

This is more natural, match should be used in user code, not case.

Fun test case to play arround with abstract predicates.

Fixes issue #20.

This is to avoid confusion with ghost_ownership.own.

This introduces n hypotheses and destructs the nth one.

This is inspired by ssr, and makes unification faster if it goes
right-to-left.

See https://sympa.inria.fr/sympa/arc/ssreflect/2013-11/msg00010.html

This way, we can use eapply instead of class_apply, which is used
when the instances are defined using the Instance command. It seems
that eapply is stronger as class_apply, and as such solves some issues
when canonical structures have type class parameters, for example:

  Goal Op (option (dec_agree nat)). apply _.

This failed, but is fixed by this commit.