Assertion failure in conseq equiv phoare with equiv in goal

[oskgo]

Hi,

Here is another example that gives me a problem.

module Foo = {
   proc foo(i : int) : int = {
      return i;
   }
}.

lemma foo_corr _i: hoare [ Foo.foo : i = _i ==> res = _i] by proc;auto.

lemma foo_eq : equiv [ Foo.foo ~ Foo.foo : ={arg} ==> ={res} ] by sim.

lemma foo_eq_corr _i :
       equiv [ Foo.foo ~ Foo.foo : ={arg} ==> ={res} /\ res{1} = _i ].
       conseq foo_eq  (foo_corr _i).

In this case the error is

anomaly: File "src/ecAst.ml", line 344, characters 45-51: Assertion failed

This causes a breaking change, although not so widespread as before.
The question is what is the best way to incorporate a hoare result into an equiv result.

Originally posted by @mbbarbosa in #837 (comment)