Bug on extra metavariable in rule RHS

[Rehan-MALAK]

Dear all,
There might be a bug with metavariables :

U : Type.
u : U.
f : U -> U.

(; h has a simple type ;)
h : U -> (U -> U) -> U.

(; hx has a dependent type ;)
def Ux : U -> Type.
[x] Ux x --> U.
hx : x:U -> (Ux x -> U) -> U.

(; rules with LHS type = RHS type = U ;)
def g : U -> U.
[i] g i --> h  u f.
[i] g i --> h  i f.
[i] g i --> hx u f.
[i] g i --> hx i f.
[i] g i --> h  u (dummy : U =>u).
[i] g i --> h  i (dummy : U =>u).
[i] g i --> hx u (dummy : U =>u).
[i] g i --> hx i (dummy : U =>u).
[i] g i --> h  u (dummy     =>u).
[i] g i --> h  i (dummy     =>u).
[i] g i --> hx u (dummy     =>u).
[i] g i --> hx i (dummy     =>u).

The last rule works with dedukti but not with lambdapi.
Here is the minimal reproduction of the problem in lambdapi syntax :

constant symbol U : TYPE
constant symbol u : U
symbol Ux : U ⇒ TYPE
rule Ux _ → U
constant symbol hx : ∀ (x : U), (Ux x ⇒ U) ⇒ U
symbol g : U ⇒ U
// set debug +su
rule g &i → hx &i (λ_  , u)

[fblanqui]

A temporary solution is to write rule g &i → hx &i (λ_:U, u).