Anomaly when instantiating lemma: module quantification

[mbbarbosa]

The code below gives an anomaly in the current main.

anomaly: File "src/ecEnv.ml", line 1595, characters 13-19: Assertion failed

Instantiating the lemma without the move fails without anomaly. I would also like to understand why.

type in_t.
type out_t.

module type RO_Pub = { proc h(x : in_t) : out_t }.

module type S_t(OO : RO_Pub) = {
 include RO_Pub
}.

module type A_t(O : RO_Pub) = {
   proc foo() : bool
}.

section.

declare module A <: A_t.
declare module S <: S_t {-A}.
lemma foo (OO <: RO_Pub {-A, -S}):
  (forall (O <: RO_Pub {-A, -S, -OO}), islossless O.h => islossless S(O).h) =>
  (forall (O <: RO_Pub {-A, -S, -OO}), islossless O.h => islossless A(O).foo) =>
  islossless OO.h =>
  islossless A(S(OO)).foo.
move => S_ll A_ll OO_ll.
move : (S_ll OO OO_ll) => SOO_ll.
apply (A_ll (S(OO)) SOO_ll).

[strub]

Offending commit is: ef42e9d9877a08228717729ff6f757b0c2269926