Improve solve_proper a bit.

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.
1 job for master
Status Job ID Name Coverage
  Test
passed #484
coq
buildjob

00:03:48