Anomaly in conseq variant after r2025.11

[mbbarbosa]

The following use of conseq results in an anomaly in r2025.11 but not in r2025.10:

module Foo = {
   proc foo1(i : int) : int = {
     while (0 < i) {
             i <- i - 1;
     }
     return i;
   }
   proc foo2(i : int) : int = {
     return 0;
   }
}.

lemma foo_1_2_eq : equiv [ Foo.foo1 ~ Foo.foo2 : ={arg} /\ 0 < i{1} ==> ={res}].
proof. proc; while {1} (0 <= i{1}) (i{1}); auto => /> /#. qed.

lemma foo2_ll : islossless Foo.foo2 by islossless.

lemma foo1_ll : islossless Foo.foo1.
conseq foo_1_2_eq foo2_ll.

[oskgo]

This is a duplicate of #834.

It will be addressed by #837.