% 2017-05-02
% Strong normalization for simply-typed lambda-calculus in Beluga

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

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 renStep : {g1 : cxt}{g2:cxt}{#R : [g2 |-# g1]}
              {M:[g1 |- tm A[]]}{M':[g1 |- tm A[]]}
              [g1 |- step M M'] -> [g2 |- step M[#R] M'[#R]] =
mlam g1, g2, #R, M, N => fn s => case s of
| [g1 |- rbeta] => [g2 |- rbeta]
| [g1 |- rabs \x.S] =>
    let [g2, x:tm _ |- S'] = renStep [g1, x: tm _ ] [g2, x:tm _ ] [g2, x:tm _ |- #R[..], x] [g1,x:tm _ |- _ ] [g1, x:tm _ |- _ ] [g1, x:tm _ |- S] in
     [g2 |- rabs \x. S']
| [g1 |- rappl S] =>
   let [g2 |- S'] = renStep [g1] [g2] [g2 |- #R] [g1 |- _ ] [g1 |- _ ] [g1 |- S] in
     [g2 |- rappl S']
| [g1 |- rappr S] =>
   let [g2 |- S'] = renStep [g1] [g2] [g2 |- #R] [g1 |- _ ] [g1 |- _ ] [g1 |- S] in
     [g2 |- rappr S']
;

rec invRenStep : {g1 : cxt} {M : [g1 |- tm A[]]} {#R : [g2 |-# g1]}
    [g2 |- step M[#R] M'] -> ExStep [g1 |- M] [g2 |- #R] [g2 |- M'] =

%   / total m (invRenStep g1 g2 a m' m) /
   %% Totality checker does not see termination -- coverage error possibly due to renaming subst.

  mlam g1, M, #R => fn s =>

  %% We would like to split on s:[g2 |- step M[rho] M'],
  %% but since Beluga's implementation of matching and unification does not take advantage of the fact that rho is a simply a renaming, it cannot unify step M[rho] M' with any of the types of step; we therefore go the longer route and split on M first; then (app M1 M2)[rho] will be normalized to app M1[rho] M2[rho] and matching on the types of step will succeed.
  case [ g1 |- M ] of

    %% Case application
    | [g1 |- app M1 M2] =>

      % Cannot reconstruct type:
      % let ih : {#R : [g2 |-# g1]}  [g2 |- step (M1[#R]) M'] ->
      %          ExStep [g1 |- M] [g2 |- #R] [g2 |- M']
      %        = invRenStep [g1] [g1 |- M1] in

      %% We case on the function part.
      (case [g1 |- M1] of

      %% Case beta-redex
      | [g1 |- abs \ x. M1'] =>
        (case s of
        %% We either contract the beta-redex...
        | [g2 |- rbeta] => Ex [g1 |- rbeta]
        %% ... or reduce in the left or right subterm
        | [g2 |- rappl S] =>
            let Ex [g1 |- S'] = % ih [g2 |- #R] [g2 |- S]
              invRenStep [g1] [g1 |- M1] [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappl S' ]
        | [g2 |- rappr S] =>
            let Ex [g1 |- S'] = invRenStep [g1] [g1 |- M2]  [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappr S' ]
        )

      %% Case not beta-redex
      | [g1 |- M1] => (case s of
        %% We either reduce in the left subterm ...
        | [g2 |- rappl S] =>
            let Ex [g1 |- S'] = invRenStep [g1] [g1 |- M1] [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappl S' ]
        %% ... or in the right subterm.
        | [g2 |- rappr S] =>
            let Ex [g1 |- S'] = invRenStep [g1] [g1 |- M2] [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappr S' ]
        )
      )

    %% Case abstraction: reduction is in function body.
    | [g1 |- abs \x. M1] => let [g2 |- rabs \y. S] = s in
          let Ex [g1, x : tm A[] |- S'] =
            invRenStep [g1, x : tm _]
              [g1, x : tm _ |- M1] [g2, x : tm _ |- #R[..], x] [g2, y : tm _ |- S ] in
          Ex [g1 |- rabs \x. S']

    % Case variable: does not reduce
    | [g1 |- #p ] => impossible s
;

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

% Lemma: closure of SN under renaming.
%
% Let Γ₂ ⊢ ρ : Γ₁.
% If Γ₁ ⊢ M ∈ SN then Γ₂ ⊢ [ρ]M ∈ SN.
% By induction on M ∈ SN.
% We show [ρ]M ∈ SN by assuming [ρ]M ⇒ M' and proving M' ∈ SN.
% Assume [ρ]M ⇒ M'.
% Then M ⇒ N with M' = [ρ]N.
% By IH on N ∈ SN, [ρ]N ∈ SN, thus, M' ∈ SN.
% QED.
rec renSN : {g2 : cxt} {#R : [g2 |-# g1]}{A:[ |- ty]} {M : [g1 |- tm A[]]}
       SN [g1 |- M]
    -> SN [g2 |- M[#R]] =
  % / total s (renSN g1 g2 a r m s) /  %% Totality checker not prepared for wf-induction.
  mlam g2, #R, A, M => fn s => let s : SN [g1 |- M] = s in
    case s of
    | Acc f => Acc (mlam M', R0 =>
        let Ex [g1 |- S] = invRenStep [g1] [g1 |- M] [g2 |- #R] [g2 |- R0]
        in  renSN [g2] [g2 |- #R] [ |- _] [g1 |- _] (f [g1 |- _] [g1 |- S])
      )
;

rec weakSN: {g: cxt} {M : [g |- tm A[]]} SN [g |- M] -> SN [g, x: tm B[] |- M[..]] =
    ?
;

rec exchange_helper: {g : cxt} {M : [g, x:tm A[], y:tm A'[] |- tm B[]]}
			       {M' : [g, x:tm A[], y:tm A'[] |- tm B[]]}
			       SN [g, y:tm A'[], x:tm A[] |- M[..,x,y]] -> [g, x:tm A[], y:tm A'[] |- step M M']
		     -> SN [g, x:tm A[], y:tm A'[] |- M'] =
    mlam g => mlam M => mlam M' => fn sn => fn s =>
    let Acc f = sn in ?

and exchangeSN: {g : cxt} {M : [g, x:tm A[], y:tm A'[] |- tm B[]]}
                SN [g, y:tm A'[], x:tm A[] |- M[..,x,y]] -> SN [g, x:tm A[], y:tm A'[] |- M] = 
    mlam g => mlam M => fn sn => Acc (mlam M', R => exchange_helper [_] [_ |- M] [_ |- M'] sn [_ |- R])
;


%% We show two fundamental properties simultaneously:
empty: type.

rec varDontStep : {g:cxt}{A : [|- ty]}
			 {#p : [g |- tm A[]]}
			 {M : [g |- tm A[]]}
			 [g |- step #p M] -> [|- empty] =
    mlam g => mlam A => mlam p => mlam M => fn s => impossible s;

% We cannot inline and directly prove that s of type [g |- step #p M'] does not step, as reconstruction will fail -- factoring the proof works.
rec varSn : {g:cxt}{A: [|- ty]}
		   {#p : [g |- tm A[]]}
		   SN [g |- #p] =
    mlam g => mlam A => mlam #p =>
    Acc (mlam M', S => impossible (varDontStep [_] [|- _] [_ |- #p] [_ |- M'] [_ |- S]))
;

rec prop5a : {g:cxt}{A : [|- ty]}{B : [|- ty]}
		    {M : [g |- tm (arr A[] B[])]}
		    {N : [g |- tm A[]]}
		    SN [g |- (app M N)] -> SN [g |- M] =
    mlam g, A, B, M, N => fn sn => case sn of
| Acc r  => Acc (mlam M' => mlam S =>
		 let sn' = r [g |- app M' N] [g |- rappl S] in
		 prop5a [_] [|- _] [|- _] [_ |- M'] [_ |- _] sn')
;

rec prop5b : {g:cxt}{A : [|- ty]}{B : [|- ty]}
		    {M : [g |- tm (arr A[] B[])]}
		    {N : [g |- tm A[]]}
		    SN [g |- (app M N)] -> SN [g |- N] =
    mlam g, A, B, M, N => fn sn =>
case sn of
| Acc r => Acc (mlam N' => mlam S =>
		let sn' = r [g |- app M N'] [g |- rappr S] in
		prop5b [_] [|- _] [|- _] [_ |- _] [_ |- N'] sn')
;

rec prop6 : {g:cxt}{A : [|- ty]}{B : [|- ty]}
		   {M : [g, x : tm A[] |- tm B[]]}
		   SN [g |- abs (\x. M)] -> SN [g, x : tm A[] |- M] =
    mlam g => mlam A => mlam B => mlam M => fn sn =>
    case sn of
    | Acc r => Acc (mlam M' => mlam S => let sn' = r [g |- abs (\x. M')] [g |- rabs (\x.S)] in
					 prop6 [_] [|- _] [|- _] [_ |- M'] sn')
;

rec prop3_helper : {g:cxt}{A : [|- ty]}{B : [|- ty]}
			  {M : [g, x : tm A[] |- tm B[]]}
			  {M' : [g |- tm (arr A[] B[])]}
			  SN [g, x : tm A[] |- M] -> [g |- step (abs (\x.M)) M'] -> SN [g |- M'] =
    mlam g => mlam A => mlam B => mlam M => mlam M' => fn sn => fn s =>
    let [g |- rabs (\x. S1)] = s in
    let Acc r = sn in
    let [g, x : tm A[] |- S1] : [g, x : tm A[] |- step M M1] = [g, x : tm A[] |- S1] in
    let sn' = r [g, x : tm A[] |- M1] [g, x : tm A[] |- S1] in
    prop3 [_] [|- _] [|- _] [_ |- M1] sn'

and prop3 : {g:cxt}{A : [|- ty]}{B : [|- ty]}
		   {M : [g, x : tm A[] |- tm B[]]}
		   SN [g, x : tm A[] |- M] -> SN [g |- abs (\x.M)] =
    mlam g => mlam A => mlam B => mlam M => fn sn =>
    case sn of
    | Acc r => Acc (mlam M' => mlam S => prop3_helper [_] [|- _] [|- _] [_ |- M] [_ |- M'] sn [_ |- S])
;

rec prop2 : {g:cxt}{A : [|- ty]} {B : [|- ty]}
   {M : [g, x : tm A[] |- tm B[]]}
   {N : [g |- tm A[]]}
   SN [g |- M [.., N] ]
   -> SN [g, x : tm A[] |- M ] =
    mlam g, A, B, M, N => fn sn =>
    case [g, x : tm A[] |- M] of
    | [g, x : tm A[] |- #p[..]] => varSn [g, x : tm A[]] [|- _] [g, x : tm A[] |- #p[..]]
    | [g, x : tm A[] |- x] => varSn [g, x : tm A[]] [|- _] [g, x : tm A[] |- x]
    | [g, x : tm A[] |- abs (\y. M')] =>
      let [|- arr A' B'] = [|- B] in
      let sn' = prop6 [g] [|- A'] [|- B'] [g, y:tm A'[] |- M'[.., (N[..]), y]] sn in
      let sn'' = prop2 [g, y:tm A'[]] [|- A] [|- B'] [g, y:tm A'[], x:tm A[] |- M'[.., x,y]] [g, y:tm A'[] |- N[..]] sn' in
      let sn''' = exchangeSN [g] [g, x: tm A[], y : tm A'[] |- M'] sn'' in 
       prop3 [g, x:tm A[]] [|- _] [|- B'] [g, x:tm A[], y:tm A'[] |- M'] sn''' %  exchange

    | [g, x : tm A[] |- app M1 M2] => let sn1 = prop5a [_] [|- _] [|- _] [_ |- M1[.., N]] [_ |- M2[.., N]] sn in
				      let sn2 = prop5b [_] [|- _] [|- _] [_ |- M1[.., N]] [_ |- M2[.., N]] sn in
				      let sn1' = prop2 [_] [|- _] [|- _] [_ |- M1] [_ |- N] sn1 in
				      let sn2' = prop2 [_] [|- _] [|- _] [_ |- M2] [_ |- N] sn2 in
				      prop1 [_] [|- _] [|- _] [_ |- M1] [_ |- M2] sn1' sn2'

and prop1_helper : {g:cxt}{A : [|- ty]}{B : [|- ty]}
			  {M : [g |- tm (arr A[] B[])]}
			  {N : [g |- tm A[]]}
			  {Q : [g |- tm B[]]}
			  {S : [g |- step (app M N) Q]}
			  SN [g |- M] -> SN [g |- N] -> SN [g |- Q] =
    mlam g => mlam A => mlam B => mlam M => mlam N => mlam Q => mlam S =>
    fn sn1 => fn sn2 =>
    let Acc r1 = sn1 in
    let Acc r2 = sn2 in
    case [g |- S] of
    | [g |- rbeta] => let [g |- abs (\x.M')] = [g |- M] in
		      let sn = prop6 [_] [|- _] [|- _] [_ |- M'] sn1 in
		      prop4 [_] [|- _] [|- _] [_ |- M'] [_ |- N] sn sn2
    | [g |- rappl S'] => let [g |- S'] : [g |- step M M'] = [g |- S'] in
			 let sn = r1 [g |- M'] [g |- S'] in
			 prop1 [_] [|- _] [|- _] [_ |- M'] [_ |- N] sn sn2
    | [g |- rappr S'] => let [g |- S'] : [g |- step N N'] = [g |- S'] in
			 let sn = r2 [g |- N'] [g |- S'] in
			 prop1 [_] [|- _] [|- _] [_ |- M] [_ |- N'] sn1 sn

and prop1 : {g:cxt}{A : [|- ty]}{B : [|- ty]}
		   {M : [g |- tm (arr A[] B[])]}
		   {N : [g |- tm A[]]}
		   SN [g |- M] -> SN [g |- N] -> SN [g |- (app M N)] =
    mlam g, A, B, M, N => fn sn1 => fn sn2 =>
    Acc (mlam M', S => prop1_helper [_] [|- _] [|- _] [_ |- M] [_ |- N] [_ |- M'] [_ |- S] sn1 sn2)

and prop4 : {g:cxt}{A: [|- ty]}{B : [|- ty]}
		   {M : [g, x : tm A[] |- tm B[]]}
		   {N : [g |- tm A[]]}
		   SN [g, x : tm A[] |- M] -> SN [g |- N] -> SN [g |-M[.., N]] =
    mlam g, A, B, M, N => fn sn1 => fn sn2 =>
    (case [g, x : tm A[] |- M] of
     | [g, x : tm A[] |- #p[..]] => varSn [_] [|- _] [_ |- #p[..]]
     | [g, x : tm A[] |- x] => sn2
     | [g, x : tm A[] |- abs (\y. M1)] =>
       let sn = prop6 [_] [|- _] [|- _] [_ |- M1] sn1 in
       let sn : SN [g, x:tm A[], y:tm A'[] |- M1] = sn in
       let exc = exchangeSN [g] [g, y: tm A'[], x:tm A[] |- M1[..,x,y]] sn in
       let sn'' = prop4 [_] [|- _] [|- _] [g, y:tm _, x:tm _ |- M1[..,x,y]] [_ |- N[..]] exc
			(weakSN [_] [_ |- N] sn2) in
       prop3 [_] [|- _] [|- _] [g, y:tm A'[] |- M1[..,N[..],y]] sn''
     | [g, x : tm A[] |- app M1 M2] => let snl = prop5a [_] [|- _] [|- _] [_ |- M1] [_ |- M2] sn1 in
				       let snr = prop5b [_] [|- _] [|- _] [_ |- M1] [_ |- M2] sn1 in
				       let sn1' = prop4 [_] [|- _] [|- _] [_ |- M1] [_ |- N] snl sn2 in
				       let sn2' = prop4 [_] [|- _] [|- _] [_ |- M2] [_ |- N] snr sn2 in
				       prop1 [_] [|- _] [|- _] [_ |- M1[.., N]] [_ |- M2[.., N]] sn1' sn2'
    )
;

rec antiSubstSN : {M : [g, x : tm A[] |- tm B[]]}
		      {N : [g |- tm A[]]}SN [g |- M [.., N] ]
		  -> SN [g, x : tm A[] |- M ] =
    mlam M => mlam N => fn sn =>
    prop2 [_] [|- _] [|- _] [_ |- M] [_ |- N] sn
;

  
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]
  ;

%% Closure of Red under renaming
%% (uses closure of SN under renaming and Kripke definition)

rec renRed : {g2 : cxt} {#R : [g2 |-# g1]}
       Red [|- A[]] [g1 |- M]
    -> Red [|- A[]] [g2 |- M[#R]] =
  mlam g2, #R => fn r =>
  let r : Red [|- A[]] [g1 |- M] = r in
  case r of
    | RBase s => RBase (renSN [g2] [g2 |- #R] [ |- _ ][g1 |- M] s)
    | RArr  f => RArr (mlam g', #R', N => fn r => f [g'] [g' |- #R[#R']] [g' |- N] r)
  ;

%% Closure of RedS under renaming (pointwise from Red)

rec renRedS : {g2 : cxt} {#R : [g2 |-# g1]}
       RedS [g] [g1 |- #S    ]
    -> RedS [g] [g2 |- #S[#R]] =
  mlam g2, #R => fn s => case s of
    | RNil       => RNil
    | RCons r s' => RCons (renRed  [g2] [g2 |- #R] r)
                          (renRedS [g2] [g2 |- #R] s')
  ;

%% Lemmata for fundamental theorem

%% Variable case

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

%% Application

rec fundApp : %% {g : cxt} {M : [g |- tm (arr A[] B[])]} {N : [g |- tm A}
          Red [|- arr A B ] [g |- M ]
       -> Red [|- A]        [g |- N ]
       -> Red [|- B]        [g |- app M N ] =
  fn r, s => let s : Red [|- B] [g |- N] = s in   %% fake match to bind g and N
    let RArr f = r in
    f [g] [ g |- .. ] [g |- N] s
  ;

%% Abstraction

%% If SN [g |- app M x] then SN [g |- M]
rec appSN : {g:cxt}{A:[ |- ty]}{B:[ |- ty]}{M:[g |- tm (arr A[] B[])]} SN [g,x:tm A[] |- app M[..] x] -> SN [g |- M] =
mlam g, A, B, M => fn s =>
 let Acc s' = s in
   Acc (mlam Q, S0 =>
         let [g, x:tm _ |- S0'] = renStep [g] [g, x:tm A[]] [g, x:tm A[] |- ..]
                                         [g |- M] [g |- Q] [g |- S0] in
        let sq = s' [g, x:tm A[] |- _ ] [g,x:tm A[] |- rappl S0'] in
               appSN [g] [ |- _ ] [|- _] [g |- _] sq
)
 ;

LF eq: tm A ->  tm A -> type =
 refl : eq  M M;

% Applicative contexts

LF ecxt : (tm A -> tm B) -> type =
  | eid  : ecxt \ x. x
  | eext : ecxt C -> ecxt \ x. app (C x) M

;

inductive ExEcxt : (g:cxt) [g |- tm A[]] -> ctype =
| ExECxt : {#p:[g |- tm B[]]}{C: [g, x:tm B[] |- tm A[]]}
           [g |- eq C[.., #p] M]
        -> [g |- ecxt \x.C]
        -> ExEcxt [g |- M];

rec ecxtEx: {g:cxt}{#p:[g |- tm A[]]}{C: [g, x:tm A[] |- tm (arr B1[] B2[])]}
           [g |- step (app C[.., #p] P) R] -> [g |- ecxt \x.C]
         -> ExEcxt [g |- R] =
mlam g, #p, C => fn s, e => case e of
| [g |- eid] : [g |- ecxt \x.x] => let [g |- S] = s in impossible [g |- S]
| [g |- eext E'] : [g |-  ecxt \x.app C Q[..]] =>
  (case s of
   | [g |- rappr S] =>
     let [g |- S] : [g |- step N N'] = [g |- S] in
     ExECxt [g |- #p] [g, x:tm _ |- app (app (C[ .., x]) Q[..]) N'[..]] [g |- refl]
            [g |- eext (eext E')]
   | [g |- rappl S]  =>
     let ExECxt [g |- #p] [g, x:tm _ |- C'] [g |- refl] [g |- E] =
         ecxtEx [g] [g |- #p] [g, x:tm _ |- C] [g |- S] [g |- E']
     in
     ExECxt [g |- #p] [g, x:tm _ |-  _ ] [g |- refl] [g |- eext E]

  )
;

% If SN [g, x:tm A[] |- C[.., x]] and SN [g, x:tm A[] |- M]
% then SN [g, x:tm A[] |- app C[..,x] M]
rec snAppAux: {g:cxt}{T:[ |- ty]}{B1:[ |- ty]}{B2:[ |- ty]}
              {Q:[g |- tm B2[]]}{M:[g |- tm B1[]]}
              {C: [g, u:tm T[] |- tm (arr B1[] B2[])]}
              {#p: [g |- tm T[]]}
              {S:[g |- step (app C[.., #p] M) Q]}
              [g |- ecxt \y.C[..,y]] ->
              SN [g |- C[.., #p]] -> SN [g |- M] ->
               SN [g |- Q] =
mlam g, T, B1, B2, Q, M, C, #p,  S => fn e, s1, s2 =>
 let [g |- #p] : [g |- tm T[]] = [g |- #p] in
 case e  of
 | [g |- eid ] : [g |- ecxt \x.x] =>  impossible [g |- S] % seems fishy ...
 | [g |- eext E'] : [g |-  ecxt \x.app C[..,x] P[..]] =>  case [g |- S] of
   | [g |- rappr S'] =>
     let Acc s2' = s2 in
     let sn2'    = s2' [g |- _ ] [g |- S'] in
       snApp [g] [g, x:tm T[] |- app C[..,x] P[..]] [g |- eext E'] [g |- #p] s1 sn2'

   | [g |- rappl S'] =>
     let Acc s1' = s1 in
     let sn1'    = s1' [g |- _ ] [g |- S'] in
     let ExECxt [g |- #p ] [g, x:tm T[] |- C'] r e' =
           ecxtEx [g] [g |- #p] [g, x: tm _ |- C] [g |- S'] [g |- E'] in
     let [g |- refl] = r in
% Need to know that if step (app C[.., #p] P) M' then
% there exists C' s.t. M' = C'[.., #p] and E0: ecxt \y.C'
% -- then we can appeal the the IH
       snApp [g] [g, x:tm T[] |- C'] e' [g |- #p] sn1' s2

and snApp : {g:cxt}{C: [g, u:tm T[] |- tm (arr B1[] B2[])]}
            [g |- ecxt \y.C] ->
            {#p: [g |- tm T[]]}
            SN [g |- C[.., #p]] -> SN [g |- M]
         -> SN [g |- app C[.., #p] M] =
mlam g, C => fn e => mlam #p => fn s1, s2 => Acc (mlam Q, S =>
  snAppAux [g] [ |- _ ] [ |- _ ] [ |- _ ] [g |- Q ]
              [g |- _] [g, x:tm _ |- C] [g |- #p]   [g |- S] e  s1 s2

)
 ;

rec snAppWk: {g:cxt}{A:[ |- ty]}{C: [g, u:tm A[] |- tm (arr B1[] B2[])]}
             {#p:[g |- tm A[]]}
             {E:[g |- ecxt \y.C]}
             {g':cxt}{#R:[g' |-# g]}{M:[g' |- tm B1[]]}
             SN [g' |- M] -> SN [g |- C[.., #p]] ->
             SN [g' |- app C[#R, #p[#R]] M] =
mlam g, A, C, #p, E, g', #R, M => fn s2, s1 =>
 let s1' = renSN [g'] [g' |- #R] [|- arr _ _] [g |- C[.., #p]] s1 in
 snApp [g'] [g', u:tm A[] |- C[#R[..],u]] [g' |- E[#R]] [g' |- #p[#R]] s1' s2
;

rec redSn: {g:cxt}{A:[ |- ty]}{M:[g |- tm A[]]}
         Red [|- A] [g |- M] -> SN [g |- M] =
mlam g, A, M => fn r => case [ |- A] of
| [ |- base] => let RBase s = r in s
| [ |- arr A B] =>
  let RArr f = r in
  let vsn = varSn [g, x:tm A[]] [|- A] [g, x : tm A[] |- x] in
  let vred = neutSn [g, x:tm A[]] [|- A] [ |- A]
                    [g, x:tm A[], y:tm A[] |- y] [g, x:tm A[] |- x] [g, x:tm A[] |- eid]  vsn in
  let m = redSn [g, x:tm A[]] [|- B] [g, x:tm A[] |- app M[..] x]
           (f [g, x:tm A[]] [g, x:tm A[] |- ..] [g, x:tm A[] |- x] vred) in
   appSN [g] [ |- _ ] [ |- _ ] [g |- _ ] m

and neutSn: {g:cxt}{A:[|- ty]}{B:[ |- ty]}{C: [g, u:tm A[] |- tm B[]]}{#p:[g |- tm A[]]}
        {E:[g |- ecxt \y.C]}
        SN [g |- C[..,#p]] -> Red [ |- B] [g |- C[..,#p]] =
mlam g, A, B, C, #p, E => fn s => case [ |- B] of
| [ |- base] => RBase s
| [ |- arr B1 B2] =>
   RArr (mlam g', #R, M => fn r =>
     let rsn  = redSn [g'] [|- B1] [g' |- M] r in % SN [g' |- M]
    let asn = snAppWk [g] [|- A] [g, u:tm A[] |- C] [g |- #p] [g |- E] [g'] [g' |- #R] [g' |- M] rsn s in
      neutSn [g'] [|- A[]] [|- B2] [g', u:tm A[] |- app C[#R[..], u] M[..]] [g' |- #p[#R]]
      [g' |- eext E[#R[..]]]
      asn
	)


and neutExp: {g:cxt}{A:[|- ty]}{B:[ |- ty]}{C: [g, u:tm A[] |- tm B[]]}{N:[g |- tm A[]]}
        {E:[g |- ecxt \y.C]}
             ({M:[g |- tm B[]]}[g |- step C[..,N] M] -> Red [ |- B] [g |- M])
	     ->  Red [ |- B] [g |- C[..,N]] = 
mlam g, A, B, C, M, E => fn s => case [ |- B] of
| [ |- base] => ? % RBase s
| [ |- arr B1 B2] => ? 
%{   RArr (mlam g', #R, M => fn r =>
     let rsn  = redSn [g'] [|- B1] [g' |- M] r in % SN [g' |- M]
    let asn = snAppWk [g] [|- A] [g, u:tm A[] |- C] [g |- #p] [g |- E] [g'] [g' |- #R] [g' |- M] rsn s in
      neutSn [g'] [|- A[]] [|- B2] [g', u:tm A[] |- app C[#R[..], u] M[..]] [g' |- #p[#R]]
      [g' |- eext E[#R[..]]]
      asn
}%	
 ;
%% rec fundAbs : Red


 %%%%%%%%%%%%%%%%%%%
 %{ For neutral terms g |- M : tm A[], 
  1) If Red [ |- A[]] [g |- M' ] and M --> M' then Red [ |- A[]] [g |- M] 
  2) If Red [ |- A[]] [g |- M] and M --> M' then Red [ |- A[]] [g |- M' ]
 }%

 rec betaExpSNecxt : {g:cxt}{A : [|- ty]} {B : [|- ty]}{M: [g, x:tm A[] |- tm B[]]}{N : [g |- tm A[]]}
        {C: [g, y : tm B[] |- tm T[]]}{E : [g |- ecxt \y.C]}		    
        SN [g |- N]		       
     -> SN [g, x:tm A[] |- M ]
     -> Red [|- T] [g |- C[.., app (abs \ x. M) N]] =
    ?
;

	
rec betaExpSN : {g:cxt}{A : [|- ty]} {B : [|- ty]}{M: [g, x:tm A[] |- tm B[]]}{N : [g |- tm A[]]}
        SN [g |- N]		       
     -> SN [g, x:tm A[] |- M ]
     -> Red [|- B] [g |- app (abs \ x. M) N] =
mlam g, A, B, M, N => fn sN, sM =>
    betaExpSNecxt [g] [ |- A] [ |- B] [g, x:tm A[] |- M] [g |- N] [g, y:tm B[] |- y] [g |- eid]
           sN sM						   
 ;
 rec betaExp' : {g:cxt}{A : [|- ty]} {B : [|- ty]}{M: [g, x:tm A[] |- tm B[]]}{N : [g |- tm A[]]}
        SN [g |- N] -> Red [|- B] [g |- M [.., N] ]
     -> Red [|- B] [g |- app (abs \ x. M) N] =
 mlam g, A, B, M, N =>
 fn s, r => betaExpSN [g] [ |- A] [ |- B] [g, x:tm A[] |- M] [g |- N] s
		      (antiSubstSN [g, x:tm A[] |- M] [g |- N]
				   (redSn [g] [ |- B] [g |- M [.., N]] r))
	 ;
% Corollary: closure under beta expansion
 rec betaExp :
	 SN [g |- N]
    -> Red [|- B] [g |- M [.., N] ]
    -> Red [|- B] [g |- app (abs \ x. M) N] =
  fn s, r =>
    betaExp' [_ ] [|- _] [|- _] [_ |- _] [_ |- _] s r
  ;

%% Fundamental theorem

rec thm : {g : cxt} {M : [g |- tm A[]]}
          RedS [g] [g' |- #S0]
       -> Red [|- A] [g' |- M[#S0]] =
  mlam g, M => fn s =>
  case [g |- M ] of
  | [g |- #p ]         =>  fundVar [g] [g |- #p] s
  | {M : [g, x : tm A[] |- tm B[]]} [g |- abs \ x. M ] =>
      RArr (mlam g', #S, N => fn r =>
        betaExp
          (redSn [g'] [ |- A] [g' |- N] r)
          (thm [g, x : tm A[]] [g, x : tm A[] |- M] (RCons r (renRedS [g'] [g' |- #S] s))))
  | [g |- app M N    ] =>  fundApp (thm [g] [g |- M] s) (thm [g] [g |- N] s)
  ;
