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
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: