Variable confusion/ill typed terms with higher-order terms

[wikku]

Script:

Kind expr type.

Type mu ((expr -> expr) -> expr) -> expr.

Define foo : expr -> expr -> prop by
  foo (mu k\ E k) (mu k_\ E (o\ o)).

Theorem bar : forall E E', nabla (x : expr), foo (E x) (E' x) -> true.
  intros. case H1 (keep).

Output:

Variables: E1
H1 : foo (mu (k\E1 n1 k)) (mu (k_\E1 k_ o\o))
============================
 true

Expected:

Variables: E1
H1 : foo (mu (k\E1 n1 k)) (mu (k_\E1 n1 o\o))
============================
 true

That is, instead of n1 : expr we have k_ : expr -> expr.

The motivation is the third-order representation of λμ-calculus. foo takes a μ-term and performs structural substitution with the empty continuation under the binder, making the continuation variable unused.