Since the generalization of ssim up-to-bind (f755434).
This is a non-trivial problem, as a ssim (update_val_rel eq eq) appears, which is not equivalent to just ssim eq because of the annoying type parameter in the val case.
The coffee machine example (more specifically the coffee_ssim proof) is a good starting point to take a closer look at the problem.
Since the generalization of ssim up-to-bind (f755434).
This is a non-trivial problem, as a
ssim (update_val_rel eq eq)appears, which is not equivalent to justssim eqbecause of the annoying type parameter in thevalcase.The coffee machine example (more specifically the
coffee_ssimproof) is a good starting point to take a closer look at the problem.