Cannot split on renamed terms

[andreasabel]

% Strong normalization for simply-typed lambda-calculus in Beluga

LF ty : type =
  | base : ty
  | arr  : ty -> ty -> ty
  ;
%name ty A.

LF tm : ty -> type =
  | abs : (tm A -> tm B) -> tm (arr A B)
  | app : tm (arr A B) -> tm A -> tm B
  ;
%name tm M.

schema cxt = tm A; % some [a : ty] block tm a;

LF step : tm A -> tm A -> type =
  | rbeta : step (app (abs M) N) (M N)
  | rabs  : ({x : tm A} step (M x) (M' x)) -> step (abs M) (abs M')
  | rappl : step M M' -> step (app M N) (app M' N)
  | rappr : step N N' -> step (app M N) (app M N')
  ;

% Lemma: If [ρ]M ⇒ M' then M ⇒ N and M' = [ρ]N.

inductive ExStep : (g1 : cxt) (g2 : cxt) 
  {M : [g1 |- tm A[]]} {#R : [g2 |-# g1]} {M' : [g2 |- tm A[]]} ctype =
  | Ex : [g1 |- step M N] -> ExStep [g1 |- M] [g2 |- #R] [g2 |- N[#R]]
  ;

rec invRenStep : {#R : [g2 |-# g1]} {M : [g1 |- tm A[]]}
    [g2 |- step M[#R] M'] -> ExStep [g1 |- M] [g2 |- #R] [g2 |- M'] =
  mlam #R, M => fn s => case s of
    | [ g2 |- rbeta ] => ?
  ;

## Type Reconstruction: /home/abel/play/beluga/sn.bel ##
<unknown location>:
Leftover constraints during abstraction.