LF ty : type = 
| base : ty
| arr : ty → ty → ty;

LF tm : ty → type = 
| abs : (tm A → tm B) → tm (arr A B)
| app : tm (arr A B) → tm A → tm B;

schema cxt = 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');

LF mstep : tm A → tm A → type = 
| m-refl : mstep M M
| m-step : step M N → mstep N M' → mstep M M';

rec m-trans : (g:cxt) {M1 : [g ⊢ tm A[]]} [g ⊢ mstep M1 M] → [g ⊢ mstep M M2] → [g ⊢ mstep M1 M2] / total s1 ( m-trans g a m1 m2 m s1 ) / =
mlam M1 ⇒ fn s1 ⇒ fn s2 ⇒ case s1 of 
  | [g ⊢ m-refl] ⇒ s2
  | [g ⊢ m-step S MS] ⇒
    let  [g ⊢ MS'] = m-trans [g ⊢ _] [g ⊢ MS] s2 in [g ⊢ m-step S MS'];

rec mstep_appl : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {M' : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} [g ⊢ mstep M M'] → [g ⊢ mstep (app M N) (app M' N)] / total ms ( mstep_appl g a b m m' n ms ) / =
mlam M ⇒ mlam M' ⇒ mlam N ⇒ fn ms ⇒ case ms of 
  | [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
  | [g ⊢ m-step S MS'] ⇒
    let  [_ ⊢ MS''] = mstep_appl [_ ⊢ _] [_ ⊢ M'] [_ ⊢ N] [_ ⊢ MS'] in [g ⊢ m-step (rappl S) MS''];

rec mstep_appr : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} {N' : [g ⊢ tm A[]]} [g ⊢ mstep N N'] → [g ⊢ mstep (app M N) (app M N')] / total ms ( mstep_appr g a b m n n' ms ) / =
mlam M ⇒ mlam N ⇒ mlam N' ⇒ fn ms ⇒ case ms of 
  | [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
  | [g ⊢ m-step S MS'] ⇒
    let  [_ ⊢ MS''] = mstep_appr [_ ⊢ M] [_ ⊢ _] [_ ⊢ N'] [_ ⊢ MS'] in [g ⊢ m-step (rappr S) MS''];

rec mstep_abs : (g:cxt) {M : [g, x : tm A[] ⊢ tm B[]]} [g, x : tm A[] ⊢ mstep M M'] → [g ⊢ mstep (abs (λx. M)) (abs (λx. M'))] / total ms ( mstep_abs g a b m m' ms ) / =
mlam M ⇒ fn s1 ⇒ case s1 of 
  | [g, x : tm A[] ⊢ m-refl] ⇒ [g ⊢ m-refl]
  | [g, x : tm A[] ⊢ m-step S MS] ⇒
    let  [g ⊢ MS'] = mstep_abs [g, x : tm A[] ⊢ _] [g, x : tm A[] ⊢ MS] in 
    let  [g ⊢ S'] = [g ⊢ rabs (λx. S)] in [g ⊢ m-step S' MS'];

rec subst_mred : (g:cxt) {M : [g, x : tm A[] ⊢ tm B[]]} {N : [g ⊢ tm A[]]} {N' : [g ⊢ tm A[]]} [g ⊢ step N N'] → [g ⊢ mstep M[…, N] M[…, N']] / trust / =
mlam M ⇒ mlam N ⇒ mlam N' ⇒ fn s ⇒ case [_, x : tm _ ⊢ M] of 
  | [g, x : tm A[] ⊢ x] ⇒ let  [g ⊢ S] = s in [g ⊢ m-step S m-refl]
  | [g, x : tm A[] ⊢ #p[…]] ⇒ [g ⊢ m-refl]
  | [g, x : tm A[] ⊢ abs (λy. M)] ⇒
    let  [g ⊢ S] = s in let  [g, y : tm _ ⊢ S'] =
                                                                    subst_mred [g, y : tm _, x : tm A[] ⊢ M[…, x, y]] [g, y : tm _ ⊢ N[…]] [g, y : tm _ ⊢ N'[…]] [g, y : tm _ ⊢ S[…]] in
                                                                    mstep_abs [g, y : tm _ ⊢ _] [g, y : tm _ ⊢ S']
  | [g, x : tm A[] ⊢ app M1 M2] ⇒
    let  [g ⊢ S1] = subst_mred [g, x : tm A[] ⊢ M1] [g ⊢ N] [g ⊢ N'] s in 
    let  [g ⊢ S2] = subst_mred [g, x : tm A[] ⊢ M2] [g ⊢ N] [g ⊢ N'] s in 
    let  [g ⊢ MS1] =
    mstep_appl [g ⊢ M1[…, N]] [g ⊢ M1[…, N']] [g ⊢ M2[…, N]] [g ⊢ S1] in 
    let  [g ⊢ MS2] =
    mstep_appr [g ⊢ M1[…, N']] [g ⊢ M2[…, N]] [g ⊢ M2[…, N']] [g ⊢ S2] in m-trans [g ⊢ _] [g ⊢ MS1] [g ⊢ MS2];

inductive Sn : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype = 
| Acc : {g : cxt} {A : [ ⊢ ty]} {M : [g ⊢ tm A[]]} ({M' : [g ⊢ tm A[]]} {S : [g ⊢ step M M']} Sn [g ⊢ M']) → Sn [g ⊢ M];

rec mstep_sn : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} [g ⊢ mstep M M'] → Sn [g ⊢ M] → Sn [g ⊢ M'] / total sn ( mstep_sn g m m' ms sn ) / =
mlam M ⇒ mlam M' ⇒ fn ms ⇒ fn sn ⇒ case ms of 
  | [g ⊢ m-refl] ⇒ sn
  | [g ⊢ m-step S MS'] ⇒
    let  Acc ([g]) ([ ⊢ A]) ([g ⊢ _]) r = sn in 
    let sn' = r [_ ⊢ _] [_ ⊢ S] in mstep_sn [_ ⊢ _] [_ ⊢ M'] [_ ⊢ MS'] sn';

inductive SN : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype = 
| SNeu : SNe [g ⊢ R] → SN [g ⊢ R]
| SAbs : SN [g, x : tm A[] ⊢ M] → SN [g ⊢ abs (λx. M)]
| SRed : SNRed [g ⊢ M] [g ⊢ M'] → SN [g ⊢ M'] → SN [g ⊢ M]
and inductive SNe : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype = 
| SVar : {#p : [g ⊢ tm A[]]} SNe [g ⊢ #p]
| SApp : SNe [g ⊢ R] → SN [g ⊢ M] → SNe [g ⊢ app R M]
and inductive SNRed : {g : cxt} → {M : [g ⊢ tm A[]]} → {M' : [g ⊢ tm A[]]} → ctype = 
| SBeta : {M : [g, x : tm A[] ⊢ tm B[]]} SN [g ⊢ N] → SNRed [g ⊢ app (abs (λx. M)) N] [g ⊢ M[…, N]]
| SAppl : SNRed [g ⊢ R] [g ⊢ R'] → SNRed [g ⊢ app R M] [g ⊢ app R' M];

inductive SnRed : {g : cxt} → {M : [g ⊢ tm A[]]} → {M' : [g ⊢ tm A[]]} → ctype = 
| SnBeta : {M : [g, x : tm A[] ⊢ tm B[]]} Sn [g ⊢ N] → SnRed [g ⊢ app (abs (λx. M)) N] [g ⊢ M[…, N]]
| SnAppl : SnRed [g ⊢ M] [g ⊢ M'] → SnRed [g ⊢ app M N] [g ⊢ app M' N];

empty : type.

rec varSn : (g:cxt) {#p : [g ⊢ tm A[]]} Sn [g ⊢ #p] / total  ( varSn ) / =
mlam p ⇒ let  [_ ⊢ #p] : [g ⊢ tm A[]]= [_ ⊢ #p] in Acc [g] [ ⊢ A] [g ⊢ #p] (mlam M' ⇒ mlam S ⇒ impossible [_ ⊢ S]);

rec abs_sn : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g, x : tm A[] ⊢ tm B[]]} Sn [g, x : tm A[] ⊢ M] → Sn [g ⊢ abs (λx. M)] / total s ( abs_sn g a b m s ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ fn sn ⇒ Acc [g] [ ⊢ arr A B] [g ⊢ abs (λx. M)] (mlam Q ⇒ mlam S ⇒ 
  let  [g ⊢ rabs (λx. S1)] = [g ⊢ S] in 
  let  [g, x : tm A[] ⊢ S1] : [g, x : tm A[] ⊢ step M M1]=
  [g, x : tm _ ⊢ S1] in let  Acc ([g, x : tm A[]]) ([ ⊢ B]) ([g, x : tm A[] ⊢ M]) r =
                                                                   sn in abs_sn [g] [ ⊢ A] [ ⊢ B] [g, x : tm A[] ⊢ M1] (r [g, x : tm A[] ⊢ M1] [g, x : tm A[] ⊢ S1]));

rec app_sna : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Sn [g ⊢ app M N] → Sn [g ⊢ M] / total s ( app_sna g a b m n s ) / =
mlam M ⇒ mlam N ⇒ fn sn ⇒ 
  let  Acc ([g]) ([ ⊢ B[]]) ([g ⊢ app M N]) r = sn in Acc [_] [_ ⊢ _] [_ ⊢ _] (mlam M' ⇒ mlam S ⇒ app_sna [_ ⊢ M'] [_ ⊢ _] (r [_ ⊢ app M' N] [_ ⊢ rappl S]));

rec app_snb : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Sn [g ⊢ app M N] → Sn [g ⊢ N] / total s ( app_snb g a b m n s ) / =
mlam M ⇒ mlam N ⇒ fn sn ⇒ 
  let  Acc ([g]) ([ ⊢ B[]]) ([g ⊢ app M N]) r = sn in Acc [_] [_ ⊢ _] [_ ⊢ _] (mlam N' ⇒ mlam S ⇒ app_snb [_ ⊢ M] [_ ⊢ N'] (r [_ ⊢ app M N'] [_ ⊢ rappr S]));

rec app_abs_sn : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g, x : tm A[] ⊢ tm B[]]} {N : [g ⊢ tm A[]]} Sn [g ⊢ M[…, N]] → Sn [g ⊢ N] → Sn [g ⊢ app (abs (λx. M)) N] / total {sn1 sn2} ( app_abs_sn g a b m n sn1 sn2 ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ mlam N ⇒ fn sn1 ⇒ fn sn2 ⇒ Acc [g] [ ⊢ B] [g ⊢ app (abs (λx. M)) N] (mlam P ⇒ mlam S ⇒ case [_ ⊢ S] of 
  | [g ⊢ rbeta] ⇒ sn1
  | [g ⊢ rappl S'] ⇒
    let  [_ ⊢ rabs (λx. S'')] = [_ ⊢ S'] in 
    let  [_ ⊢ S''] : [g, x : tm _ ⊢ step M M']= [_ ⊢ S''] in 
    let  [_ ⊢ S'''] = [_ ⊢ S''[…, N]] in 
    let  Acc ([g]) ([ ⊢ B]) ([g ⊢ _]) r = sn1 in app_abs_sn [g] [ ⊢ _] [ ⊢ _] [_ ⊢ M'] [_ ⊢ N] (r [_ ⊢ M'[…, N]] [_ ⊢ S''']) sn2
  | [g ⊢ rappr S'] ⇒
    let  Acc ([g]) ([ ⊢ A]) ([g ⊢ N]) r = sn2 in 
    let  [_ ⊢ S'] : [_ ⊢ step N N']= [_ ⊢ S'] in 
    let  [_ ⊢ MS''] = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] [_ ⊢ S'] in 
    let sn' = mstep_sn [_ ⊢ M[…, N]] [_ ⊢ M[…, N']] [_ ⊢ MS''] sn1 in
    app_abs_sn [g] [ ⊢ _] [ ⊢ _] [_ ⊢ M] [_ ⊢ N'] sn' (r [_ ⊢ N'] [_ ⊢ S']));

inductive Neutral : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype = 
| Nvar : {#x : [g ⊢ tm A[]]} Neutral [g ⊢ #x]
| Napp : {R : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Neutral [g ⊢ R] → Neutral [g ⊢ app R N];

rec neu-step : (g:cxt) {R : [g ⊢ tm A[]]} {R' : [g ⊢ tm A[]]} [g ⊢ step R R'] → Neutral [g ⊢ R] → Neutral [g ⊢ R'] / total s ( neu-step g a r r' s n ) / =
mlam R ⇒ mlam R' ⇒ fn s ⇒ fn neu ⇒ case neu of 
  | Nvar ([g ⊢ #x])  ⇒ impossible s
  | Napp ([g ⊢ R'']) ([g ⊢ N]) neu'  ⇒
    case s of 
    | [g ⊢ rbeta] ⇒ impossible neu'
    | [g ⊢ rappl S'] ⇒
      let neu'' = neu-step [_ ⊢ R''] [_ ⊢ _] [_ ⊢ S'] neu' in
      Napp [_ ⊢ _] [_ ⊢ N] neu''
    | [g ⊢ rappr S'] ⇒ Napp [_ ⊢ R''] [_ ⊢ _] neu';

rec app_sn : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {R : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Neutral [g ⊢ R] → Sn [g ⊢ R] → Sn [g ⊢ N] → Sn [g ⊢ app R N] / total {sn1 sn2} ( app_sn g a b r n neu sn1 sn2 ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam R ⇒ mlam N ⇒ fn neu ⇒ fn sn1 ⇒ fn sn2 ⇒ Acc [g] [ ⊢ B] [g ⊢ app R N] (mlam Q ⇒ mlam S ⇒ case [g ⊢ S] of 
  | [g ⊢ rbeta] ⇒ impossible neu
  | [g ⊢ rappl S'] ⇒
    let  Acc ([g]) ([ ⊢ arr A B]) ([g ⊢ R]) r = sn1 in 
    let neu' = neu-step [_ ⊢ R] [_ ⊢ _] [_ ⊢ S'] neu in
    app_sn [g] [ ⊢ A] [ ⊢ B] [g ⊢ _] [g ⊢ N] neu' (r [_ ⊢ _] [_ ⊢ S']) sn2
  | [g ⊢ rappr S'] ⇒
    let  Acc ([g]) ([ ⊢ A]) ([g ⊢ N]) r = sn2 in app_sn [g] [ ⊢ A] [ ⊢ B] [_ ⊢ R] [_ ⊢ _] neu sn1 (r [_ ⊢ _] [_ ⊢ S']));

inductive ConfResult : {g : cxt} → {N : [g ⊢ tm A[]]} → {N' : [g ⊢ tm A[]]} → ctype = 
| Eq : ConfResult [g ⊢ N] [g ⊢ N]
| Conf : SnRed [g ⊢ N'] [g ⊢ Q] → [g ⊢ mstep N Q] → ConfResult [g ⊢ N] [g ⊢ N'];

rec confluence : (g:cxt) {M : [g ⊢ tm A[]]} {N : [g ⊢ tm A[]]} {N' : [g ⊢ tm A[]]} {S : [g ⊢ step M N']} SnRed [g ⊢ M] [g ⊢ N] → ConfResult [g ⊢ N] [g ⊢ N'] / total s ( confluence g a m n n' s ) / =
mlam M ⇒ mlam N ⇒ mlam N' ⇒ mlam S ⇒ fn snr ⇒ case snr of 
  | SnBeta ([g, x : tm A[] ⊢ M]) sn  ⇒
    case [g ⊢ S] of 
    | [g ⊢ rbeta] ⇒ Eq
    | [g ⊢ rappl S'] ⇒
      let  [_ ⊢ rabs (λx. S'')] = [_ ⊢ S'] in 
      let  [_ ⊢ S''] : [g, x : tm _ ⊢ step M M']= [_ ⊢ S''] in 
      let snr' = SnBeta [g, x : tm _ ⊢ M'] sn in
      let  sn : Sn [g ⊢ N]= sn in 
      let  [_ ⊢ R] = [_ ⊢ S''[…, N]] in Conf snr' [g ⊢ m-step R m-refl]
    | [g ⊢ rappr S'] ⇒
      let  [_ ⊢ S'] : [_ ⊢ step N N']= [_ ⊢ S'] in 
      let ms = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] [_ ⊢ S'] in
      let  Acc ([_]) ([ ⊢ _]) ([_ ⊢ _]) r = sn in 
      let sn' = r [_ ⊢ N'] [_ ⊢ S'] in Conf (SnBeta [g, x : tm _ ⊢ M] sn') ms
  | SnAppl r  ⇒
    case [_ ⊢ S] of 
    | [g ⊢ rbeta] ⇒ impossible r
    | [g ⊢ rappl S'] ⇒
      let conf = confluence [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ S'] r in
      case conf of 
      | Eq  ⇒ Eq
      | Conf snr' ms  ⇒
        let  snr' : SnRed [g ⊢ M2] [g ⊢ P]= snr' in 
        let ms' = mstep_appl [_ ⊢ _] [_ ⊢ P] [_ ⊢ _] ms in
        Conf (SnAppl snr') ms'
    | [g ⊢ rappr S'] ⇒
      let ms = [_ ⊢ m-step S' m-refl] in
      let  r : SnRed [_ ⊢ M] [_ ⊢ M']= r in 
      let ms' = mstep_appr [_ ⊢ M'] [_ ⊢ _] [_ ⊢ _] ms in
      Conf (SnAppl r) ms';

rec bc_aux : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g ⊢ tm (arr A[] B[])]} {M' : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Sn [g ⊢ M] → Sn [g ⊢ N] → SnRed [g ⊢ M] [g ⊢ M'] → Sn [g ⊢ app M' N] → Sn [g ⊢ app M N] / total {sn1 sn2} ( bc_aux g a b m m' n sn1 sn2 ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ mlam M' ⇒ mlam N ⇒ fn sn1 ⇒ fn sn2 ⇒ fn snr ⇒ fn sn ⇒ Acc [g] [ ⊢ B] [g ⊢ app M N] (mlam Q ⇒ mlam S ⇒ case [g ⊢ S] of 
  | [g ⊢ rbeta] ⇒ impossible snr
  | [g ⊢ rappl S'] ⇒
    let conf = confluence [_ ⊢ M] [_ ⊢ M'] [_ ⊢ _] [_ ⊢ S'] snr in
    case conf of 
    | Eq  ⇒ sn
    | Conf snr' ms  ⇒
      let ms' = mstep_appl [_ ⊢ M'] [_ ⊢ _] [_ ⊢ N] ms in
      let sn' = mstep_sn [_ ⊢ app M' N] [_ ⊢ _] ms' sn in
      let  Acc ([g]) ([ ⊢ arr A B]) ([g ⊢ M]) r = sn1 in bc_aux [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ N] (r [_ ⊢ _] [_ ⊢ S']) sn2 snr' sn'
  | [g ⊢ rappr S'] ⇒
    let  Acc ([g]) ([ ⊢ B]) ([g ⊢ app M' N]) r = sn in 
    let sn' = r [_ ⊢ _] [_ ⊢ rappr S'] in
    let  Acc ([g]) ([ ⊢ A]) ([g ⊢ N]) r' = sn2 in bc_aux [_] [ ⊢ _] [ ⊢ _] [_ ⊢ M] [_ ⊢ M'] [_ ⊢ _] sn1 (r' [_ ⊢ _] [_ ⊢ S']) snr sn');

rec backwards_closure : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} SnRed [g ⊢ M] [g ⊢ M'] → Sn [g ⊢ M'] → Sn [g ⊢ M] / total r ( backwards_closure g a m m' r ) / =
mlam M ⇒ mlam M' ⇒ fn snr ⇒ fn sn ⇒ case snr of 
  | SnBeta ([g, x : tm A[] ⊢ M]) sn'  ⇒ app_abs_sn [_] [ ⊢ _] [ ⊢ _] [_ ⊢ M] [_ ⊢ _] sn sn'
  | SnAppl r  ⇒
    let snl' = app_sna [_ ⊢ _] [_ ⊢ _] sn in
    let snl = backwards_closure [_ ⊢ _] [_ ⊢ _] r snl' in
    let snr = app_snb [_ ⊢ _] [_ ⊢ _] sn in
    bc_aux [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] snl snr r sn;

rec neutralSNe : (g:cxt) {R : [g ⊢ tm A[]]} SNe [g ⊢ R] → Neutral [g ⊢ R] / total sne ( neutralSNe g a r sne ) / =
mlam R ⇒ fn sne ⇒ case sne of 
  | SVar ([g ⊢ #p])  ⇒ Nvar [g ⊢ #p]
  | SApp sne' sn  ⇒
    let neu = neutralSNe [_ ⊢ _] sne' in Napp [_ ⊢ _] [_ ⊢ _] neu;

rec soundSN : (g:cxt) {M : [g ⊢ tm A[]]} SN [g ⊢ M] → Sn [g ⊢ M] / total s ( soundSN g a m s ) / =
mlam M ⇒ fn sn ⇒ case sn of 
  | SNeu sne  ⇒ soundSNe [_ ⊢ M] sne
  | SAbs sn'  ⇒
    let sn'' = soundSN [_ ⊢ _] sn' in abs_sn [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] sn''
  | SRed snr sn'  ⇒
    let snr' = soundSNRed [_ ⊢ _] [_ ⊢ _] snr in
    let sn'' = soundSN [_ ⊢ _] sn' in backwards_closure [_ ⊢ M] [_ ⊢ _] snr' sn''
and soundSNe : (g:cxt) {M : [g ⊢ tm A[]]} SNe [g ⊢ M] → Sn [g ⊢ M] / total s ( soundSNe g a m s ) / =
mlam M ⇒ fn sne ⇒ case sne of 
  | SVar ([g ⊢ #p])  ⇒ varSn [g ⊢ #p]
  | SApp sne' sn  ⇒
    let snl = soundSNe [_ ⊢ _] sne' in
    let snr = soundSN [_ ⊢ _] sn in
    let neu = neutralSNe [_ ⊢ _] sne' in
    app_sn [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] neu snl snr
and soundSNRed : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} SNRed [g ⊢ M] [g ⊢ M'] → SnRed [g ⊢ M] [g ⊢ M'] / total s ( soundSNRed g a m m' s ) / =
mlam M ⇒ mlam M' ⇒ fn snr ⇒ case snr of 
  | SBeta ([g, x : tm A[] ⊢ M]) sn  ⇒
    let sn' = soundSN [_ ⊢ _] sn in SnBeta [_ ⊢ M] sn'
  | SAppl snr'  ⇒
    let snr'' = soundSNRed [_ ⊢ _] [_ ⊢ _] snr' in SnAppl snr'';

rec renameSN : {g : cxt} {g' : cxt} [g' ⊢ g] {M : [g ⊢ tm A[]]} SN [g ⊢ M] → SN [g' ⊢ M[#R]] / total s ( renameSN g g' a r m s ) / =
mlam g ⇒ mlam g' ⇒ mlam R ⇒ mlam M ⇒ fn s ⇒ case s of 
  | SNeu s'  ⇒ SNeu (renameSNe [g' ⊢ #R] [g ⊢ M] s')
  | SAbs s'  ⇒
    SAbs (renameSN [g, x : tm _] [g', x : tm _] [g', x : tm _ ⊢ #R[…], x] [g, x : tm _ ⊢ _] s')
  | SRed r s'  ⇒ SRed (renameSNRed [g' ⊢ #R] [g ⊢ M] r) (renameSN [g] [g'] [g' ⊢ #R] [g ⊢ _] s')
and renameSNe : (g:cxt) (g':cxt) [g' ⊢ g] {M : [g ⊢ tm A[]]} SNe [g ⊢ M] → SNe [g' ⊢ M[#R]] / total s ( renameSNe g g' a r m s ) / =
mlam R ⇒ mlam M ⇒ fn s ⇒ case s of 
  | SVar ([g ⊢ #p])  ⇒ SVar [_ ⊢ #p[#R]]
  | SApp s1 s2  ⇒
    SApp (renameSNe [_ ⊢ #R] [_ ⊢ _] s1) (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s2)
and renameSNRed : (g:cxt) (g':cxt) [g' ⊢ g] {M : [g ⊢ tm A[]]} SNRed [g ⊢ M] [g ⊢ N] → SNRed [g' ⊢ M[#R]] [g' ⊢ N[#R]] / total s ( renameSNRed g g' a r m s ) / =
mlam R ⇒ mlam M ⇒ fn s ⇒ case s of 
  | SBeta ([g, x : tm A[] ⊢ M]) s'  ⇒
    SBeta [_, x : tm A[] ⊢ M[#R[…], x]] (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s')
  | SAppl s'  ⇒ SAppl (renameSNRed [_ ⊢ #R] [_ ⊢ _] s');

inductive SNRed' : {g : cxt} → {g' : cxt} → [g' ⊢ g] → {M : [g ⊢ tm A[]]} → {M' : [g' ⊢ tm A[]]} → ctype = 
| SNRed' : {g' : cxt} {g : cxt} {N : [g ⊢ tm A[]]} SNRed [g ⊢ M] [g ⊢ N] → SNRed' [g' ⊢ #R] [g ⊢ M] [g' ⊢ N[#R]];

rec anti_renameSNe : (g:cxt) (g':cxt) [g' ⊢ g] {M : [g ⊢ tm A[]]} SNe [g' ⊢ M[#R]] → SNe [g ⊢ M] / total s ( anti_renameSNe g g' a r m s ) / =
mlam R ⇒ mlam N ⇒ fn s ⇒ case s of 
  | SVar ([h' ⊢ _])  ⇒ SVar [_ ⊢ _]
  | SApp r s  ⇒
    let r' = anti_renameSNe [_ ⊢ #R] [_ ⊢ _] r in
    let s' = anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s in SApp r' s'
and anti_renameSNRed : {g : cxt} {g' : cxt} [g' ⊢ g] {M : [g ⊢ tm A[]]} SNRed [g' ⊢ M[#R]] [g' ⊢ N'] → SNRed' [g' ⊢ #R] [g ⊢ M] [g' ⊢ N'] / total s ( anti_renameSNRed g g' a r m s ) / =
mlam g ⇒ mlam g' ⇒ mlam R ⇒ mlam M ⇒ fn r ⇒ case r of 
  | SBeta ([_ ⊢ _]) s  ⇒
    let s' = anti_renameSN [g] [g'] [g' ⊢ #R] [_ ⊢ _] s in
    SNRed' [_] [_] [_ ⊢ _] (SBeta [_ ⊢ _] s')
  | SAppl r'  ⇒
    let  SNRed' ([_]) ([_]) ([_ ⊢ _]) r0 =
    anti_renameSNRed [g] [g'] [g' ⊢ #R] [_ ⊢ _] r' in SNRed' [_] [_] [_ ⊢ _] (SAppl r0)
and anti_renameSN : {g : cxt} {g' : cxt} [g' ⊢ g] {M : [g ⊢ tm A[]]} SN [g' ⊢ M[#R]] → SN [g ⊢ M] / total s ( anti_renameSN g g' a r m s ) / =
mlam g ⇒ mlam g' ⇒ mlam R ⇒ mlam M ⇒ fn s ⇒ case s of 
  | SAbs s'  ⇒
    SAbs (anti_renameSN [g, x : tm _] [g', x : tm _] [g', x : tm _ ⊢ #R[…], x] [g, x : tm _ ⊢ _] s')
  | SNeu s'  ⇒ SNeu (anti_renameSNe [g' ⊢ #R] [g ⊢ M] s')
  | SRed r' s'  ⇒
    let  SNRed' ([g']) ([g]) ([g ⊢ N]) r =
    anti_renameSNRed [_] [_] [g' ⊢ #R] [_ ⊢ _] r' in 
    let s'' = anti_renameSN [g] [g'] [g' ⊢ #R] [g ⊢ N] s' in SRed r s'';

rec ext_SN : {M : [g ⊢ tm (arr A[] B[])]} {#p : [g ⊢ tm A[]]} SN [g ⊢ app M (#p)] → SN [g ⊢ M] / total s ( ext_SN g a b m p s ) / =
mlam M ⇒ mlam p ⇒ fn s ⇒ case s of 
  | SNeu (SApp sm sv )  ⇒ SNeu sm
  | SRed r sm'  ⇒
    case r of 
    | SBeta ([g, x : tm A[] ⊢ M']) sn  ⇒
      let sn' =
      anti_renameSN [g, x : tm A[]] [g] [g ⊢ …, (#p[…])] [g, x : tm A[] ⊢ M'] sm' in
      SAbs sn'
    | SAppl r'  ⇒ let sn = ext_SN [_ ⊢ _] [_ ⊢ #p] sm' in SRed r' sn;

inductive Red : {A : [ ⊢ ty]} → {g : cxt} → {M : [g ⊢ tm A[]]} → ctype = 
| RBase : SN [g ⊢ M] → Red [ ⊢ base] [g ⊢ M]
| RArr : ({g' : cxt} [g' ⊢ g] {N : [g' ⊢ tm A[]]} Red [ ⊢ A] [g' ⊢ N] → Red [ ⊢ B] [g' ⊢ app M[σ] N]) → Red [ ⊢ arr A B] [g ⊢ M];

inductive RedS : {g : cxt} → {g' : cxt} → [g' ⊢ g] → ctype = 
| RNil : RedS [] [g' ⊢ ^]
| RCons : Red [ ⊢ A] [g' ⊢ M] → RedS [g] [g' ⊢ σ] → RedS [g, x : tm A[]] [g' ⊢ σ, M];

rec rename_red : {g : cxt} {g' : cxt} {A : [ ⊢ ty]} {M : [g ⊢ tm A[]]} [g' ⊢ g] Red [ ⊢ A] [g ⊢ M] → Red [ ⊢ A] [g' ⊢ M[#R]] / total a ( rename_red g g' a ) / =
mlam g ⇒ mlam g' ⇒ mlam A ⇒ mlam M ⇒ mlam R ⇒ fn r ⇒ case [ ⊢ A] of 
  | [ ⊢ base] ⇒
    let  RBase s = r in RBase (renameSN [_] [_] [g' ⊢ #R] [g ⊢ M] s)
  | [ ⊢ arr A B] ⇒
    let  RArr r' = r in RArr (mlam g'' ⇒ mlam S ⇒ mlam N ⇒ fn rn ⇒ r' [g''] [g'' ⊢ #R[σ[…]]] [g'' ⊢ N] rn)
and rename_redS : {g : cxt} {g' : cxt} [g' ⊢ g] RedS [h] [g ⊢ σ] → RedS [h] [g' ⊢ σ[#R]] / total rs ( rename_redS g g' s rs ) / =
mlam g ⇒ mlam g' ⇒ mlam R ⇒ fn rs ⇒ case rs of 
  | RNil  ⇒ RNil
  | RCons r rs'  ⇒
    RCons (rename_red [g] [g'] [ ⊢ _] [_ ⊢ _] [g' ⊢ #R] r) (rename_redS [g] [g'] [g' ⊢ #R] rs');

rec cr1 : {g : cxt} {A : [ ⊢ ty]} {M : [g ⊢ tm A[]]} Red [ ⊢ A] [g ⊢ M] → SN [g ⊢ M] / total a ( cr1 g a ) / =
mlam g ⇒ mlam A ⇒ mlam M ⇒ fn r ⇒ case [ ⊢ A] of 
  | [ ⊢ base] ⇒ let  RBase s = r in s
  | [ ⊢ arr A B] ⇒
    let rv =
    cr3 [g, x : tm A[]] [ ⊢ A] [g, x : tm A[] ⊢ x] (SVar [g, x : tm A[] ⊢ x]) in
    let  RArr r' = r in 
    let s =
    cr1 [g, x : tm A[]] [ ⊢ B] [g, x : tm A[] ⊢ app M[…] x] (r' [g, x : tm A[]] [g, x : tm A[] ⊢ …] [g, x : tm A[] ⊢ x] rv) in
    let sm = ext_SN [g, x : tm A[] ⊢ M[…]] [g, x : tm A[] ⊢ x] s in
    anti_renameSN [_] [_] [g, x : tm A[] ⊢ …] [g ⊢ M] sm
and cr2 : {g : cxt} {A : [ ⊢ ty]} {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} SNRed [g ⊢ M] [g ⊢ M'] → Red [ ⊢ A] [g ⊢ M'] → Red [ ⊢ A] [g ⊢ M] / total a ( cr2 g a ) / =
mlam g ⇒ mlam A ⇒ mlam M ⇒ mlam M' ⇒ fn sr ⇒ fn rm' ⇒ case [ ⊢ A] of 
  | [ ⊢ base] ⇒ let  RBase sm' = rm' in RBase (SRed sr sm')
  | [ ⊢ arr A B] ⇒
    let  RArr rm' = rm' in RArr (mlam g' ⇒ mlam R ⇒ mlam N ⇒ fn rn ⇒ cr2 [g'] [ ⊢ B] [g' ⊢ app M[#R] N] [g' ⊢ app M'[#R] N] (SAppl (renameSNRed [g' ⊢ #R] [g ⊢ M] sr)) (rm' [g'] [g' ⊢ #R] [g' ⊢ N] rn))
and cr3 : {g : cxt} {A : [ ⊢ ty]} {M : [g ⊢ tm A[]]} SNe [g ⊢ M] → Red [ ⊢ A] [g ⊢ M] / total a ( cr3 g a ) / =
mlam g ⇒ mlam A ⇒ mlam M ⇒ fn sm ⇒ case [ ⊢ A] of 
  | [ ⊢ base] ⇒ RBase (SNeu sm)
  | [ ⊢ arr A B] ⇒
    RArr (mlam g' ⇒ mlam R ⇒ mlam N ⇒ fn rn ⇒ 
    let sn = cr1 [g'] [ ⊢ A] [g' ⊢ N] rn in
    cr3 [g'] [ ⊢ B] [g' ⊢ app M[#R] N] (SApp (renameSNe [g' ⊢ #R] [g ⊢ M] sm) sn));

rec red_var : {g : cxt} {#p : [g ⊢ tm A[]]} Red [ ⊢ A] [g ⊢ #p] / total  ( red_var ) / =
mlam g ⇒ mlam p ⇒ cr3 [_] [ ⊢ _] [_ ⊢ _] (SVar [g ⊢ #p]);

rec fundVar : {g : cxt} {#p : [g ⊢ tm A[]]} RedS [g] [g' ⊢ σ] → Red [ ⊢ A] [g' ⊢ #p[σ]] / total g ( fundVar g ) / =
mlam g ⇒ mlam 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';

rec fundamental_lemma : {g : cxt} {g' : cxt} {M : [g ⊢ tm A[]]} [g' ⊢ g] RedS [g] [g' ⊢ σ] → Red [ ⊢ A[]] [g' ⊢ M[σ]] / total m ( fundamental_lemma g g' a m ) / =
mlam g ⇒ mlam g' ⇒ mlam M ⇒ mlam S ⇒ fn rs ⇒ case [g ⊢ M] of 
  | [g ⊢ #p] ⇒ fundVar [g] [g ⊢ #p] rs
  | [g ⊢ app M N] ⇒
    let  RArr r1 = fundamental_lemma [g] [g'] [g ⊢ M] [g' ⊢ σ] rs in 
    let r2 = fundamental_lemma [g] [g'] [g ⊢ N] [g' ⊢ σ] rs in r1 [g'] [g' ⊢ …] [g' ⊢ N[σ]] r2
  | [g ⊢ abs (λx. M)] ⇒
    RArr (mlam g'' ⇒ mlam R ⇒ mlam N ⇒ fn rn ⇒ 
    let rs' = rename_redS [g'] [g''] [g'' ⊢ #R] rs in
    let r =
    fundamental_lemma [g, x : tm _] [g''] [g, x : tm _ ⊢ M] [g'' ⊢ σ[#R], N] (RCons rn rs') in
    let sn = cr1 [_] [ ⊢ _] [_ ⊢ _] rn in
    let sn' = SBeta [g'', x : tm _ ⊢ M[σ[#R[…]], x]] sn in
    cr2 [_] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] sn' r);

rec id_red : {g : cxt} RedS [g] [g ⊢ …] / total g ( id_red g ) / =
mlam g ⇒ case [g] of 
  | [] ⇒ RNil
  | [g, x : tm A[]] ⇒
    let r = id_red [g] in
    let r' = rename_redS [g] [g, x : tm A[]] [g, x : tm A[] ⊢ …] r in
    RCons (red_var [g, x : tm A[]] [g, x : tm A[] ⊢ x]) r';

rec norm : {g : cxt} {M : [g ⊢ tm A[]]} SN [g ⊢ M] / total  ( norm ) / =
mlam g ⇒ mlam M ⇒ cr1 [_] [ ⊢ _] [_ ⊢ _] (fundamental_lemma [g] [g] [g ⊢ M] [g ⊢ …] (id_red [g]));

To download the code: sn.bel