Since the generalization of ssim up-to-bind (f7554343c5f58d93f492115b745687df132f1c17).
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 (f7554343c5f58d93f492115b745687df132f1c17).
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.