Should this work? `context in the body appears to be more general than the context supplied`

[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.

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')
  ;

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

inductive SN : (g : cxt) {M : [ g |- tm A ]} ctype =
  | Acc : ({M' : [ g |- tm A ]} [ g |- step M M' ] -> SN [ g |- M' ])
        -> SN [ g |- M ]
  ;

stratified Red : {A : [ |- ty ]} (g : cxt) {M : [ g |- tm A[] ]} ctype =
  | RBase : SN [g |- M] -> Red [ |- base ] [g |- M]
  | RArr  : ({g' : cxt} {#S : [g' |-# g]} {N : [g' |- tm A[]]}
               Red [|- A] [g' |- N]
            -> Red [|- B] [g' |- app M[#S] N])
         -> Red [ |- arr A B ] [g |- M]
  ;

inductive RedS : {g : cxt} (g' : cxt) {#S : [g' |- g]} ctype =
  | RNil  : RedS [] [ g' |- ^ ]
  | RCons : Red [|- A] [g' |- M]
         -> RedS [g] [g' |- #S]
         -> RedS [g, x : tm A[]] [g' |- #S, M]
  ;

%% Lemmata for fundamental theorem

rec fundVar : {g : cxt} {#p : [g |- tm A[]]}
          RedS [g] [g' |- #S]
       -> Red [|- A] [g' |- #p[#S]] =
  mlam g, #p => fn s => case s of
    | RNil       => impossible [ |- #p ]
    | RCons r s' => case [g |- #p] of
      | [g, x : tm A[] |- x     ] => r
      | [g, x : tm A[] |- #q[..]] => fundVar [g] [g |- #q] s'
  ;