Swiss army knife for inversion

[YaZko]

Inversion of equivalent computations is painful, we currently have a whole bunch of lemmas and keep doing things in an ad-hoc way. We need a tactic settling it once and for all (at least for [equ], hopefully for [sbisim] too).

Need to cover:

• Cases where both computations exhibit a head constructor
  -- Unifies the arguments if suitable
  -- Derives a contradiction if not
• Cases where only one side exhibit a head constructor
  -- Derives the head constructor of the other computation