LF ty : type = 
| base : ty
| arr : ty → ty → ty
| sum : 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
| inl : {B : ty} (tm A → tm (sum A B))
| inr : {A : ty} (tm B → tm (sum A B))
| match : tm (sum A B) → (tm A → tm C) → (tm B → tm C) → tm C;

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')
| rinl : step M N → step (inl B M) (inl B N)
| rinr : step M N → step (inr A M) (inr A N)
| rcase : step M M' → step (match M N1 N2) (match M' N1 N2)
| rcinl : step (match (inl B M) N1 N2) (N1 M)
| rcinr : step (match (inr A M) N1 N2) (N2 M)
| rcl : ({x : tm A} (step (N x) (N' x))) → step (match M N N2) (match M N' N2)
| rcr : ({x : tm B} (step (N x) (N' x))) → step (match M N1 N) (match M N1 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 mstep_inl : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} {B : [ ⊢ ty]} [g ⊢ mstep M M'] → [g ⊢ mstep (inl B[] M) (inl B[] M')] / total ms ( mstep_inl g a m m' b ms ) / =
mlam M ⇒ mlam M' ⇒ mlam B ⇒ fn ms ⇒ case ms of 
  | [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
  | [g ⊢ m-step S MS'] ⇒
    let  [_ ⊢ MS''] = mstep_inl [_ ⊢ _] [_ ⊢ _] [ ⊢ B] [_ ⊢ MS'] in [g ⊢ m-step (rinl S) MS''];

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

rec mstep_match : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {M' : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} [g ⊢ mstep M M'] → [g ⊢ mstep (match M (λx. N1) (λy. N2)) (match M' (λx. N1) (λy. N2))] / total ms ( mstep_match g a b c m m' n1 n2 ms ) / =
mlam M ⇒ mlam M' ⇒ mlam N1 ⇒ mlam N2 ⇒ fn ms ⇒ case ms of 
  | [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
  | [g ⊢ m-step S MS] ⇒
    let  [_ ⊢ MS'] = mstep_match [_ ⊢ _] [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ N2] [_ ⊢ MS] in [g ⊢ m-step (rcase S) MS'];

rec mstep_matchl : (g:cxt) {N : [g, x : tm A[] ⊢ tm C[]]} {N' : [g, x : tm A[] ⊢ tm C[]]} {M : [g ⊢ tm (sum A[] B[])]} {N2 : [g, y : tm B[] ⊢ tm C[]]} [g, x : tm A[] ⊢ mstep N N'] → [g ⊢ mstep (match M (λx. N) (λy. N2)) (match M (λx. N') (λy. N2))] / total ms ( mstep_matchl g a c b n n' m n2 ms ) / =
mlam N ⇒ mlam N' ⇒ mlam M ⇒ mlam N2 ⇒ fn ms ⇒ case ms of 
  | [g, x : tm A[] ⊢ m-refl] ⇒ [g ⊢ m-refl]
  | [g, x : tm A[] ⊢ m-step S MS] ⇒
    let  [_ ⊢ MS'] = mstep_matchl [_ ⊢ _] [_ ⊢ N'] [_ ⊢ M] [_ ⊢ N2] [_ ⊢ MS] in [g ⊢ m-step (rcl (λx. S)) MS'];

rec mstep_matchr : (g:cxt) {N : [g, x : tm B[] ⊢ tm C[]]} {N' : [g, x : tm B[] ⊢ tm C[]]} {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, y : tm A[] ⊢ tm C[]]} [g, x : tm B[] ⊢ mstep N N'] → [g ⊢ mstep (match M (λx. N1) (λy. N)) (match M (λx. N1) (λy. N'))] / total ms ( mstep_matchr g b c a n n' m n1 ms ) / =
mlam N ⇒ mlam N' ⇒ mlam M ⇒ mlam N1 ⇒ fn ms ⇒ case ms of 
  | [g, x : tm B[] ⊢ m-refl] ⇒ [g ⊢ m-refl]
  | [g, x : tm B[] ⊢ m-step S MS] ⇒
    let  [_ ⊢ MS'] = mstep_matchr [_ ⊢ _] [_ ⊢ N'] [_ ⊢ M] [_ ⊢ N1] [_ ⊢ MS] in [g ⊢ m-step (rcr (λx. 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]
  | [g, x : tm A[] ⊢ inl B[] M] ⇒
    let  [_ ⊢ MS] = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] s in mstep_inl [g ⊢ M[…, N]] [g ⊢ M[…, N']] [ ⊢ B] [_ ⊢ MS]
  | [g, x : tm A[] ⊢ inr B[] M] ⇒
    let  [_ ⊢ MS] = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] s in mstep_inr [_ ⊢ _] [_ ⊢ _] [ ⊢ B] [_ ⊢ MS]
  | [g, x : tm A[] ⊢ match M (λx. N1) (λy. N2)] ⇒
    let  [_ ⊢ S] = s in let  [_ ⊢ S0] =
                                                                    subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] s in 
    let  [g, y : tm B[] ⊢ S1] =
    subst_mred [g, y : tm _, x : tm A[] ⊢ N1[…, x, y]] [g, y : tm _ ⊢ N[…]] [g, y : tm _ ⊢ N'[…]] [g, y : tm _ ⊢ S[…]] in
    let  [g, y : tm C[] ⊢ S2] =
    subst_mred [g, y : tm _, x : tm A[] ⊢ N2[…, x, y]] [g, y : tm _ ⊢ N[…]] [g, y : tm _ ⊢ N'[…]] [g, y : tm _ ⊢ S[…]] in
    let  [g, x : tm A[], y : tm B[] ⊢ N1'] = [_ ⊢ N1] in 
    let  [g ⊢ MS0] =
    mstep_match [g ⊢ M[…, N]] [g ⊢ M[…, N']] [g, y : tm B[] ⊢ N1[…, N[…], y]] [g, y : tm C[] ⊢ N2[…, N[…], y]] [_ ⊢ S0] in
    let  [g ⊢ MS1] =
    mstep_matchl [g, y : tm B[] ⊢ N1[…, N[…], y]] [g, y : tm B[] ⊢ N1[…, N'[…], y]] [g ⊢ M[…, N']] [g, y : tm C[] ⊢ N2[…, N[…], y]] [_ ⊢ S1] in
    let  [g ⊢ MS2] =
    mstep_matchr [g, y : tm C[] ⊢ N2[…, N[…], y]] [g, y : tm C[] ⊢ N2[…, N'[…], y]] [g ⊢ M[…, N']] [g, y : tm B[] ⊢ N1[…, N'[…], y]] [_ ⊢ S2] in
    m-trans [_ ⊢ _] [_ ⊢ MS0] (m-trans [_ ⊢ _] [_ ⊢ MS1] [_ ⊢ 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]
| SInl : SN [g ⊢ M] → SN [g ⊢ inl _ M]
| SInr : SN [g ⊢ M] → SN [g ⊢ inr _ 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]
| SCase : SNe [g ⊢ M] → SN [g, x : tm A[] ⊢ N1] → SN [g, y : tm B[] ⊢ N2] → SNe [g ⊢ match M (λx. N1) (λy. N2)]
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]
| SCInl : SN [g ⊢ M] → SN [g, x : tm A[] ⊢ N1] → SN [g, y : tm B[] ⊢ N2] → SNRed [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] [g ⊢ N1[…, M]]
| SCInr : SN [g ⊢ M] → SN [g, x : tm A[] ⊢ N1] → SN [g, y : tm B[] ⊢ N2] → SNRed [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] [g ⊢ N2[…, M]]
| SRCase : SNRed [g ⊢ M] [g ⊢ M'] → {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} SNRed [g ⊢ match M (λx. N1) (λy. N2)] [g ⊢ match M' (λx. N1) (λy. N2)];

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]
| SnCInl : Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → SnRed [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] [g ⊢ N1[…, M]]
| SnCInr : Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → SnRed [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] [g ⊢ N2[…, M]]
| SnCasR : SnRed [g ⊢ M] [g ⊢ M'] → {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} SnRed [g ⊢ match M (λx. N1) (λy. N2)] [g ⊢ match M' (λx. N1) (λy. N2)];

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 inl_sn : (g:cxt) {M : [g ⊢ tm A[]]} {B : [ ⊢ ty]} Sn [g ⊢ M] → Sn [g ⊢ inl B[] M] / total sn ( inl_sn g a m b sn ) / =
mlam M ⇒ mlam B ⇒ fn sn ⇒ 
  let  Acc ([g]) ([ ⊢ A[]]) ([g ⊢ M]) r = sn in Acc [g] [ ⊢ sum A B] [g ⊢ inl B[] M] (mlam M' ⇒ mlam S ⇒ 
  let  [g ⊢ rinl S'] = [g ⊢ S] in inl_sn [_ ⊢ _] [ ⊢ B] (r [_ ⊢ _] [_ ⊢ S']));

rec inr_sn : (g:cxt) {M : [g ⊢ tm B[]]} {A : [ ⊢ ty]} Sn [g ⊢ M] → Sn [g ⊢ inr A[] M] / total sn ( inr_sn g b m a sn ) / =
mlam M ⇒ mlam A ⇒ fn sn ⇒ 
  let  Acc ([g]) ([ ⊢ B[]]) ([g ⊢ M]) r = sn in Acc [g] [ ⊢ sum A B] [g ⊢ inr A[] M] (mlam M' ⇒ mlam S ⇒ 
  let  [g ⊢ rinr S'] = [g ⊢ S] in inr_sn [_ ⊢ _] [ ⊢ A] (r [_ ⊢ _] [_ ⊢ S']));

rec case_sna : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ match M (λx. N1) (λy. N2)] → Sn [g ⊢ M] / total sn ( case_sna g a b c m n1 n2 sn ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn ⇒ 
  let  [_ ⊢ M] : [g ⊢ tm (sum A[] B[])]= [_ ⊢ M] in 
  let  Acc ([g]) ([ ⊢ C]) ([g ⊢ match M (λx. N1) (λy. N2)]) r = sn in Acc [g] [ ⊢ sum A[] B[]] [g ⊢ M] (mlam M' ⇒ mlam S ⇒ case_sna [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ rcase S]));

rec case_snb : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ match M (λx. N1) (λy. N2)] → Sn [g, x : tm A[] ⊢ N1] / total sn ( case_snb g a b c m n1 n2 sn ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn ⇒ 
  let  [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in 
  let  Acc ([g]) ([ ⊢ C]) ([g ⊢ match M (λx. N1) (λy. N2)]) r = sn in Acc [g, x : tm A[]] [ ⊢ C] [g, x : tm A[] ⊢ N1] (mlam N1' ⇒ mlam S ⇒ case_snb [_ ⊢ M] [_ ⊢ N1'] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ rcl (λx. S)]));

rec case_snc : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ match M (λx. N1) (λy. N2)] → Sn [g, y : tm B[] ⊢ N2] / total sn ( case_snc g a b c m n1 n2 sn ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn ⇒ 
  let  [_ ⊢ N2] : [g, y : tm B[] ⊢ tm C[]]= [_ ⊢ N2] in 
  let  Acc ([g]) ([ ⊢ C]) ([g ⊢ match M (λx. N1) (λy. N2)]) r = sn in Acc [g, y : tm B[]] [ ⊢ C] [g, y : tm B[] ⊢ N2] (mlam N2' ⇒ mlam S ⇒ case_snc [_ ⊢ M] [_ ⊢ N1] [_ ⊢ N2'] (r [_ ⊢ _] [_ ⊢ rcr (λy. 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 {sn2 sn1} ( 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]
| Ncase : {R : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Neutral [g ⊢ R] → Neutral [g ⊢ match R (λx. N1) (λy. N2)];

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'
  | Ncase ([g ⊢ R'']) ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2]) neu'  ⇒
    case s of 
    | [g ⊢ rcase S'] ⇒
      let neu'' = neu_step [_ ⊢ R''] [_ ⊢ _] [_ ⊢ S'] neu' in
      Ncase [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] neu''
    | [g ⊢ rcinl] ⇒ impossible neu'
    | [g ⊢ rcinr] ⇒ impossible neu'
    | [g ⊢ rcl (λx. S')] ⇒ Ncase [_ ⊢ R''] [_ ⊢ _] [_ ⊢ N2] neu'
    | [g ⊢ rcr (λy. S')] ⇒ Ncase [_ ⊢ R''] [_ ⊢ N1] [_ ⊢ _] 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 [_ ⊢ _] [_ ⊢ _] [_ ⊢ 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']));

rec match_sn : (g:cxt) {R : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Neutral [g ⊢ R] → Sn [g ⊢ R] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → Sn [g ⊢ match R (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( match_sn g a b c r n1 n2 neu sn0 sn1 sn2 ) / =
mlam R ⇒ mlam N1 ⇒ mlam N2 ⇒ fn neu ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒ 
  let  [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in Acc [g] [ ⊢ C] [g ⊢ match R (λx. N1) (λy. N2)] (mlam M' ⇒ mlam S ⇒ case [g ⊢ S] of 
  | [g ⊢ rcase S'] ⇒
    let  Acc ([g]) ([ ⊢ sum A[] B[]]) ([g ⊢ R]) r = sn0 in 
    let neu' = neu_step [_ ⊢ _] [_ ⊢ _] [_ ⊢ S'] neu in
    match_sn [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] neu' (r [_ ⊢ _] [_ ⊢ S']) sn1 sn2
  | [g ⊢ rcinl] ⇒ impossible neu
  | [g ⊢ rcinr] ⇒ impossible neu
  | [g ⊢ rcl (λx. S')] ⇒
    let  Acc ([g, x : tm A[]]) ([ ⊢ C[]]) ([g, x : tm A[] ⊢ N1]) r = sn1 in match_sn [_ ⊢ R] [_ ⊢ _] [_ ⊢ N2] neu sn0 (r [_ ⊢ _] [_ ⊢ S']) sn2
  | [g ⊢ rcr (λy. S')] ⇒
    let  Acc ([g, y : tm B[]]) ([ ⊢ C[]]) ([g, y : tm B[] ⊢ N2]) r = sn2 in match_sn [_ ⊢ R] [_ ⊢ N1] [_ ⊢ _] neu sn0 sn1 (r [_ ⊢ _] [_ ⊢ S']));

rec casel_sn : (g:cxt) {M : [g ⊢ tm A[]]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ M] → Sn [g ⊢ N1[…, M]] → Sn [g, y : tm B[] ⊢ N2] → Sn [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( casel_sn g a b c m n1 n2 sn0 sn1 sn2 ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒ 
  let  [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in 
  let  [_ ⊢ N2] : [g, y : tm B[] ⊢ tm C[]]= [_ ⊢ N2] in Acc [g] [ ⊢ C] [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] (mlam P ⇒ mlam S ⇒ case [g ⊢ S] of 
  | [g ⊢ rcase (rinl S')] ⇒
    let  Acc ([g]) ([ ⊢ A]) ([g ⊢ M]) r = sn0 in 
    let ms = subst_mred [_ ⊢ N1] [_ ⊢ M] [_ ⊢ _] [_ ⊢ S'] in
    let sn1' = mstep_sn [_ ⊢ N1[…, M]] [_ ⊢ _] ms sn1 in
    casel_sn [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ S']) sn1' sn2
  | [g ⊢ rcinl] ⇒ sn1
  | [g ⊢ rcl (λx. S')] ⇒
    let  [_ ⊢ S''] = [_ ⊢ S'[…, M]] in 
    let  Acc ([g]) ([ ⊢ C]) ([g ⊢ _]) r = sn1 in casel_sn [_ ⊢ M] [_ ⊢ _] [_ ⊢ N2] sn0 (r [_ ⊢ _] [_ ⊢ S'']) sn2
  | [g ⊢ rcr (λy. S')] ⇒
    let  Acc ([g, y : tm B[]]) ([ ⊢ C]) ([g, y : tm B[] ⊢ N2]) r = sn2 in casel_sn [_ ⊢ M] [_ ⊢ N1] [_ ⊢ _] sn0 sn1 (r [_ ⊢ _] [_ ⊢ S']));

rec caser_sn : (g:cxt) {M : [g ⊢ tm B[]]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g ⊢ N2[…, M]] → Sn [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( caser_sn g b a c m n1 n2 sn0 sn1 sn2 ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒ 
  let  [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in 
  let  [_ ⊢ N2] : [g, y : tm B[] ⊢ tm C[]]= [_ ⊢ N2] in Acc [g] [ ⊢ C] [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] (mlam P ⇒ mlam S ⇒ case [g ⊢ S] of 
  | [g ⊢ rcase (rinr S')] ⇒
    let  Acc ([g]) ([ ⊢ B]) ([g ⊢ M]) r = sn0 in 
    let ms = subst_mred [g, x : tm B[] ⊢ N2] [g ⊢ M[…]] [g ⊢ _] [g ⊢ S'] in
    let sn2' = mstep_sn [g ⊢ N2[…, M]] [g ⊢ _] ms sn2 in
    caser_sn [g ⊢ _] [g, x : tm A[] ⊢ N1] [g, x : tm B[] ⊢ N2] (r [g ⊢ _] [g ⊢ S']) sn1 sn2'
  | [g ⊢ rcinr] ⇒ sn2
  | [g ⊢ rcl (λx. S')] ⇒
    let  Acc ([g, x : tm A[]]) ([ ⊢ C]) ([g, x : tm A[] ⊢ N1]) r = sn1 in caser_sn [_ ⊢ M] [_ ⊢ _] [_ ⊢ N2] sn0 (r [_ ⊢ _] [_ ⊢ S']) sn2
  | [g ⊢ rcr (λy. S')] ⇒
    let  [_ ⊢ S''] = [_ ⊢ S'[…, M]] in 
    let  Acc ([g]) ([ ⊢ C]) ([g ⊢ _]) r = sn2 in caser_sn [_ ⊢ M] [_ ⊢ N1] [_ ⊢ _] sn0 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'
  | SnCInl sn sn1 sn2  ⇒
    let  Acc ([g]) ([ ⊢ sum A1[] A2[]]) ([g ⊢ M0]) r = sn in case [g ⊢ S] of 
    | [g ⊢ rcase (rinl S')] ⇒
      let sn' = r [_ ⊢ _] [_ ⊢ S'] in
      let snr' = SnCInl sn' sn1 sn2 in
      let  Acc ([_]) ([ ⊢ _]) ([_ ⊢ N1]) r = sn1 in 
      let ms = subst_mred [_ ⊢ N1] [_ ⊢ M0] [_ ⊢ _] [_ ⊢ S'] in Conf snr' ms
    | [g ⊢ rcinl] ⇒ Eq
    | [g ⊢ rcl (λx. S')] ⇒
      let  [_ ⊢ S'] : [g, x : tm _ ⊢ step N1 N1']= [_ ⊢ S'] in 
      let  [_ ⊢ S''] = [_ ⊢ S'[…, M0]] in 
      let  Acc ([g, x : tm A[]]) ([ ⊢ C]) ([g, x : tm A[] ⊢ N1]) r = sn1 in 
      let sn1' = r [_ ⊢ N1'] [_ ⊢ S'] in
      let snr' = SnCInl sn sn1' sn2 in
      Conf snr' [g ⊢ m-step S'' m-refl]
    | [g ⊢ rcr (λy. S')] ⇒
      let  Acc ([g, y : tm A2[]]) ([ ⊢ C[]]) ([g, y : tm A2[] ⊢ N2]) r' = sn2 in 
      let sn2' = r' [_ ⊢ _] [_ ⊢ S'] in
      let snr' = SnCInl sn sn1 sn2' in Conf snr' [g ⊢ m-refl]
  | SnCInr sn sn1 sn2  ⇒
    let  Acc ([g]) ([ ⊢ sum A1[] A2[]]) ([g ⊢ M0]) r = sn in case [g ⊢ S] of 
    | [g ⊢ rcase (rinr S')] ⇒
      let sn' = r [_ ⊢ _] [_ ⊢ S'] in
      let  Acc ([_]) ([ ⊢ _]) ([_ ⊢ N2]) r = sn2 in 
      let snr' = SnCInr sn' sn1 sn2 in
      let ms = subst_mred [_ ⊢ N2] [_ ⊢ M0] [_ ⊢ _] [_ ⊢ S'] in Conf snr' ms
    | [g ⊢ rcinr] ⇒ Eq
    | [g ⊢ rcl (λx. S')] ⇒
      let  Acc ([g, x : tm A1[]]) ([ ⊢ C[]]) ([g, x : tm A1[] ⊢ N1]) r' = sn1 in 
      let sn1' = r' [_ ⊢ _] [_ ⊢ S'] in
      let  Acc ([_]) ([ ⊢ _]) ([_ ⊢ N2]) r = sn2 in 
      let snr' = SnCInr sn sn1' sn2 in Conf snr' [g ⊢ m-refl]
    | [g ⊢ rcr (λx. S')] ⇒
      let  [_ ⊢ S'] : [g, x : tm _ ⊢ step N2 N2']= [_ ⊢ S'] in 
      let  [_ ⊢ S''] = [_ ⊢ S'[…, M0]] in 
      let  Acc ([g, y : tm B[]]) ([ ⊢ C]) ([g, y : tm B[] ⊢ N2]) r = sn2 in 
      let sn2' = r [_ ⊢ N2'] [_ ⊢ S'] in
      let snr' = SnCInr sn sn1 sn2' in
      Conf snr' [g ⊢ m-step S'' m-refl]
  | SnCasR snr' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2])  ⇒
    case [g ⊢ S] of 
    | [g ⊢ rcase S'] ⇒
      let conf = confluence [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ S'] snr' in
      case conf of 
      | Eq  ⇒ Eq
      | Conf snr'' ms  ⇒
        let  [_ ⊢ MS] = mstep_match [_ ⊢ _] [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] ms in Conf (SnCasR snr'' [_ ⊢ N1] [_ ⊢ N2]) [_ ⊢ MS]
    | [g ⊢ rcinl] ⇒ impossible snr'
    | [g ⊢ rcinr] ⇒ impossible snr'
    | [g ⊢ rcl (λx. S')] ⇒
      let  [_ ⊢ S'] : [g, x : tm _ ⊢ step N1 N1']= [_ ⊢ S'] in 
      let snr'' = SnCasR snr' [_ ⊢ N1'] [_ ⊢ N2] in
      let  snr' : SnRed [g ⊢ M] [g ⊢ M']= snr' in 
      let ms =
      mstep_matchl [_ ⊢ N1] [_ ⊢ N1'] [_ ⊢ M'] [_ ⊢ N2] [_ ⊢ m-step S' m-refl] in
      Conf snr'' ms
    | [g ⊢ rcr (λy. S')] ⇒
      let  [_ ⊢ S'] : [g, x : tm _ ⊢ step N2 N2']= [_ ⊢ S'] in 
      let snr'' = SnCasR snr' [_ ⊢ N1] [_ ⊢ N2'] in
      let  snr' : SnRed [g ⊢ M] [g ⊢ M']= snr' in 
      let ms =
      mstep_matchr [_ ⊢ N2] [_ ⊢ N2'] [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ m-step S' m-refl] in
      Conf snr'' ms;

rec bc_aux_app : {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_app 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_app [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ 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_app [_] [ ⊢ _] [ ⊢ _] [_ ⊢ M] [_ ⊢ M'] [_ ⊢ _] sn1 (r' [_ ⊢ _] [_ ⊢ S']) snr sn');

rec bc_aux_sum : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {M' : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → SnRed [g ⊢ M] [g ⊢ M'] → Sn [g ⊢ match M' (λx. N1) (λy. N2)] → Sn [g ⊢ match M (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( bc_aux_sum g a b c m m' n1 n2 sn0 sn1 sn2 ) / =
mlam M ⇒ mlam M' ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒ fn snr ⇒ fn sn' ⇒ 
  let  [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in Acc [g] [ ⊢ C] [g ⊢ match M (λx. N1) (λy. N2)] (mlam Q ⇒ mlam S ⇒ case [g ⊢ S] of 
  | [g ⊢ rcase S'] ⇒
    let conf = confluence [_ ⊢ M] [_ ⊢ M'] [_ ⊢ _] [_ ⊢ S'] snr in
    case conf of 
    | Eq  ⇒ sn'
    | Conf snr' ms  ⇒
      let  [_ ⊢ MS] = mstep_match [_ ⊢ M'] [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] ms in 
      let sn'' = mstep_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ MS] sn' in
      let  Acc ([g]) ([ ⊢ _]) ([g ⊢ M]) r = sn0 in bc_aux_sum [_ ⊢ _] [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ S']) sn1 sn2 snr' sn''
  | [g ⊢ rcinl] ⇒ impossible snr
  | [g ⊢ rcinr] ⇒ impossible snr
  | [g ⊢ rcl (λx. S')] ⇒
    let  [_ ⊢ S'] : [g, x : tm _ ⊢ step N1 N1']= [_ ⊢ S'] in 
    let  Acc ([g]) ([ ⊢ _]) ([g ⊢ _]) r = sn' in 
    let sn'' = r [g ⊢ match M' (λx. N1') (λy. N2)] [g ⊢ rcl (λx. S')] in
    let  Acc ([g, x : tm _]) ([ ⊢ C]) ([g, x : tm _ ⊢ N1]) r' = sn1 in bc_aux_sum [_ ⊢ M] [_ ⊢ M'] [_ ⊢ N1'] [_ ⊢ N2] sn0 (r' [_ ⊢ N1'] [_ ⊢ S']) sn2 snr sn''
  | [g ⊢ rcr (λy. S')] ⇒
    let  [_ ⊢ S'] : [g, y : tm _ ⊢ step N2 N2']= [_ ⊢ S'] in 
    let  Acc ([g]) ([ ⊢ _]) ([g ⊢ _]) r = sn' in 
    let sn'' = r [g ⊢ match M' (λx. N1) (λy. N2')] [g ⊢ rcr (λy. S')] in
    let  Acc ([g, y : tm _]) ([ ⊢ C]) ([g, y : tm _ ⊢ N2]) r' = sn2 in bc_aux_sum [_ ⊢ M] [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ N2'] sn0 sn1 (r' [_ ⊢ N2'] [_ ⊢ 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_app [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] snl snr r sn
  | SnCInl sn0 sn1 sn2  ⇒ casel_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] sn0 sn sn2
  | SnCInr sn0 sn1 sn2  ⇒ caser_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] sn0 sn1 sn
  | SnCasR snr' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2])  ⇒
    let sn' = case_sna [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] sn in
    let sn0 = backwards_closure [_ ⊢ _] [_ ⊢ _] snr' sn' in
    let sn1 = case_snb [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] sn in
    let sn2 = case_snc [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] sn in
    bc_aux_sum [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] sn0 sn1 sn2 snr' 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
  | SCase sne' sn1 sn2  ⇒
    let neu = neutralSNe [_ ⊢ _] sne' in
    let  sn1 : SN [g, x : tm A[] ⊢ N1]= sn1 in 
    let  sn2 : SN [g, x : tm B[] ⊢ N2]= sn2 in Ncase [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] 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''
  | SInl sn'  ⇒
    let sn'' = soundSN [_ ⊢ _] sn' in inl_sn [_ ⊢ _] [ ⊢ _] sn''
  | SInr sn'  ⇒
    let sn'' = soundSN [_ ⊢ _] sn' in inr_sn [_ ⊢ _] [ ⊢ _] 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
  | SCase sne' snl snr  ⇒
    let neu = neutralSNe [_ ⊢ _] sne' in
    let sn0 = soundSNe [_ ⊢ _] sne' in
    let sn1 = soundSN [_ ⊢ _] snl in
    let sn2 = soundSN [_ ⊢ _] snr in match_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] neu sn0 sn1 sn2
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''
  | SCInl sn0 sn1 sn2  ⇒
    let sn0' = soundSN [_ ⊢ _] sn0 in
    let sn1' = soundSN [_ ⊢ _] sn1 in
    let sn2' = soundSN [_ ⊢ _] sn2 in SnCInl sn0' sn1' sn2'
  | SCInr sn0 sn1 sn2  ⇒
    let sn0' = soundSN [_ ⊢ _] sn0 in
    let sn1' = soundSN [_ ⊢ _] sn1 in
    let sn2' = soundSN [_ ⊢ _] sn2 in SnCInr sn0' sn1' sn2'
  | SRCase snr' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2])  ⇒
    let snr'' = soundSNRed [_ ⊢ _] [_ ⊢ _] snr' in SnCasR snr'' [_ ⊢ N1] [_ ⊢ N2];

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')
  | SInl s'  ⇒ SInl (renameSN [g] [g'] [g' ⊢ #R] [g ⊢ _] s')
  | SInr s'  ⇒ SInr (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)
  | SCase s1 s2 s3  ⇒
    SCase (renameSNe [_ ⊢ #R] [_ ⊢ _] s1) (renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_, x : tm _ ⊢ _] s2) (renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_, y : tm _ ⊢ _] s3)
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')
  | SCInl s' n1 n2  ⇒
    SCInl (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s') (renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_, x : tm _ ⊢ _] n1) (renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_, y : tm _ ⊢ _] n2)
  | SCInr s' n1 n2  ⇒
    SCInr (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s') (renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_, x : tm _ ⊢ _] n1) (renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_, y : tm _ ⊢ _] n2)
  | SRCase s' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2])  ⇒
    SRCase (renameSNRed [_ ⊢ #R] [_ ⊢ _] s') [_, x : tm A[] ⊢ N1[#R[…], x]] [_, y : tm B[] ⊢ N2[#R[…], y]];

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'
  | SCase s1 s2 s3  ⇒
    let s1' = anti_renameSNe [_ ⊢ #R] [_ ⊢ _] s1 in
    let s2' =
    anti_renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_ ⊢ _] s2 in
    let s3' =
    anti_renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_ ⊢ _] s3 in
    SCase s1' s2' s3'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)
  | SCInl s n1 n2  ⇒
    let s' = anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s in
    let s1 = anti_renameSN [g, x : tm _] [_] [g', x : tm _ ⊢ #R[…], x] [_ ⊢ _] n1 in
    let s2 = anti_renameSN [g, y : tm _] [_] [g', y : tm _ ⊢ #R[…], y] [_ ⊢ _] n2 in
    SNRed' [_] [_] [_ ⊢ _] (SCInl s' s1 s2)
  | SCInr s n1 n2  ⇒
    let s' = anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s in
    let s1 = anti_renameSN [g, x : tm _] [_] [g', x : tm _ ⊢ #R[…], x] [_ ⊢ _] n1 in
    let s2 = anti_renameSN [g, y : tm _] [_] [g', y : tm _ ⊢ #R[…], y] [_ ⊢ _] n2 in
    SNRed' [_] [_] [_ ⊢ _] (SCInr s' s1 s2)
  | SRCase s ([g', x : tm _ ⊢ _]) ([g', y : tm _ ⊢ _])  ⇒
    let  SNRed' ([_]) ([_]) ([_ ⊢ _]) s' = anti_renameSNRed [_] [_] [_ ⊢ #R] [_ ⊢ _] s in SNRed' [_] [_] [_ ⊢ _] (SRCase s' [g, x : tm _ ⊢ _] [g, y : tm _ ⊢ _])
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''
  | SInl s'  ⇒ SInl (anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s')
  | SInr s'  ⇒ SInr (anti_renameSN [_] [_] [_ ⊢ #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 Eq : {g : cxt} → {y2892 : [g ⊢ tm A[]]} → {z2891 : [g ⊢ tm A[]]} → ctype = 
| Refl : Eq [g ⊢ M] [g ⊢ M];

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]
| RSum : DSClosure [g ⊢ M] → Red [ ⊢ sum A B] [g ⊢ M]
and inductive DSClosure : {g : cxt} → {M : [g ⊢ tm (sum A[] B[])]} → ctype = 
| DSLeft : Red [ ⊢ A] [g ⊢ N] → Eq [g ⊢ inl B[] N] [g ⊢ M] → DSClosure [g ⊢ M]
| DSRight : Red [ ⊢ B] [g ⊢ N] → Eq [g ⊢ inr A[] N] [g ⊢ M] → DSClosure [g ⊢ M]
| DSSNe : SNe [g ⊢ M] → DSClosure [g ⊢ M]
| DSRed : DSClosure [g ⊢ M] → SNRed [g ⊢ N] [g ⊢ M] → DSClosure [g ⊢ N];

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)
  | [ ⊢ sum A B] ⇒
    let  RSum d = r in RSum (rename_DS [g] [g'] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [g' ⊢ #R] d)
and rename_DS : {g : cxt} {g' : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g ⊢ tm (sum A[] B[])]} [g' ⊢ g] DSClosure [g ⊢ M] → DSClosure [g' ⊢ M[#R]] / total d ( rename_DS g g' a b m r d ) / =
mlam g ⇒ mlam g' ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ mlam R ⇒ fn d ⇒ case d of 
  | DSLeft r' (Refl )  ⇒
    DSLeft (rename_red [g] [g'] [ ⊢ _] [_ ⊢ _] [g' ⊢ #R] r') Refl
  | DSRight r' (Refl )  ⇒
    DSRight (rename_red [g] [g'] [ ⊢ _] [_ ⊢ _] [g' ⊢ #R] r') Refl
  | DSSNe sne  ⇒ DSSNe (renameSNe [_ ⊢ #R] [_ ⊢ _] sne)
  | DSRed d' r'  ⇒
    let d'' = rename_DS [g] [g'] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [g' ⊢ #R] d' in
    DSRed d'' (renameSNRed [_ ⊢ #R] [_ ⊢ _] r')
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
  | [ ⊢ sum A B] ⇒ let  RSum d = r in ds_cr1 [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] d
and ds_cr1 : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g ⊢ tm (sum A[] B[])]} DSClosure [g ⊢ M] → SN [g ⊢ M] / total d ( ds_cr1 g a b m d ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ fn d ⇒ case d of 
  | DSLeft r' (Refl )  ⇒ SInl (cr1 [_] [ ⊢ _] [_ ⊢ _] r')
  | DSRight r' (Refl )  ⇒ SInr (cr1 [_] [ ⊢ _] [_ ⊢ _] r')
  | DSSNe sne  ⇒ SNeu sne
  | DSRed d' r'  ⇒
    let sn = ds_cr1 [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] d' in SRed r' sn
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))
  | [ ⊢ sum A B] ⇒ let  RSum d = rm' in RSum (DSRed d sr)
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))
  | [ ⊢ sum A B] ⇒ RSum (DSSNe sm);

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 eq_red : Eq [g ⊢ M] [g ⊢ N] → Red [ ⊢ C] [g ⊢ match M (λx. N1) (λy. N2)] → Red [ ⊢ C] [g ⊢ match N (λx. N1) (λy. N2)] / total  ( eq_red ) / =
fn e ⇒ fn r ⇒ let  Refl = e in r;

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)
  | [g ⊢ inl B[] M] ⇒
    let r = fundamental_lemma [g] [g'] [g ⊢ M] [g' ⊢ σ] rs in
    RSum (DSLeft r Refl)
  | [g ⊢ inr A[] M] ⇒
    let r = fundamental_lemma [g] [g'] [g ⊢ M] [g' ⊢ σ] rs in
    RSum (DSRight r Refl)
  | [g ⊢ match M (λx. N1) (λy. N2)] ⇒
    let r = fundamental_lemma [g] [g'] [g ⊢ M] [g' ⊢ σ] rs in
    let  RSum d = r in main_ds [g] [g'] [g' ⊢ M[σ]] [g, x : tm _ ⊢ N1] [g, y : tm _ ⊢ N2] [g' ⊢ σ] rs d
and main_ds : {g : cxt} {g' : cxt} {M : [g' ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} [g' ⊢ g] RedS [g] [g' ⊢ σ] → DSClosure [g' ⊢ M] → Red [ ⊢ C[]] [g' ⊢ match M (λx. N1[σ[…], x]) (λy. N2[σ[…], y])] / total d ( main_ds g g' m n1 n2 s rs d ) / =
mlam g ⇒ mlam g' ⇒ mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ mlam S ⇒ fn rs ⇒ fn d ⇒ case d of 
  | DSLeft r e  ⇒
    let sn0 = cr1 [_] [ ⊢ _] [_ ⊢ _] r in
    let r1 =
    fundamental_lemma [_, x : tm _] [_] [_, x : tm _ ⊢ N1] [_ ⊢ σ[…], _] (RCons r rs) in
    let r2 =
    fundamental_lemma [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ N2] [_ ⊢ σ[…], _] (RCons (red_var [g', y : tm _] [g', y : tm _ ⊢ y]) (rename_redS [g'] [g', y : tm _] [g', y : tm _ ⊢ …] rs)) in
    let r1' =
    fundamental_lemma [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ N1] [_ ⊢ σ[…], _] (RCons (red_var [g', x : tm _] [g', x : tm _ ⊢ x]) (rename_redS [g'] [g', x : tm _] [g', x : tm _ ⊢ …] rs)) in
    let sn1 = cr1 [_] [ ⊢ _] [_ ⊢ _] r1' in
    let sn2 = cr1 [_] [ ⊢ _] [_ ⊢ _] r2 in
    let snr = SCInl sn0 sn1 sn2 in
    eq_red e (cr2 [_] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] snr r1)
  | DSRight r e  ⇒
    let sn0 = cr1 [_] [ ⊢ _] [_ ⊢ _] r in
    let r1 =
    fundamental_lemma [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ N1] [_ ⊢ σ[…], _] (RCons (red_var [g', x : tm _] [g', x : tm _ ⊢ x]) (rename_redS [g'] [g', x : tm _] [g', x : tm _ ⊢ …] rs)) in
    let r2 =
    fundamental_lemma [_, y : tm _] [_] [_, y : tm _ ⊢ N2] [_ ⊢ σ[…], _] (RCons r rs) in
    let r2' =
    fundamental_lemma [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ N2] [_ ⊢ σ[…], _] (RCons (red_var [g', y : tm _] [g', y : tm _ ⊢ y]) (rename_redS [g'] [g', y : tm _] [g', y : tm _ ⊢ …] rs)) in
    let sn1 = cr1 [_] [ ⊢ _] [_ ⊢ _] r1 in
    let sn2 = cr1 [_] [ ⊢ _] [_ ⊢ _] r2' in
    let snr = SCInr sn0 sn1 sn2 in
    eq_red e (cr2 [_] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] snr r2)
  | DSSNe sne  ⇒
    let r1 =
    fundamental_lemma [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ N1] [_ ⊢ σ[…], _] (RCons (red_var [g', x : tm _] [g', x : tm _ ⊢ x]) (rename_redS [g'] [g', x : tm _] [g', x : tm _ ⊢ …] rs)) in
    let r2 =
    fundamental_lemma [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ N2] [_ ⊢ σ[…], _] (RCons (red_var [g', y : tm _] [g', y : tm _ ⊢ y]) (rename_redS [g'] [g', y : tm _] [g', y : tm _ ⊢ …] rs)) in
    let sn1 = cr1 [_] [ ⊢ _] [_ ⊢ _] r1 in
    let sn2 = cr1 [_] [ ⊢ _] [_ ⊢ _] r2 in
    let sne' = SCase sne sn1 sn2 in cr3 [_] [ ⊢ _] [_ ⊢ _] sne'
  | DSRed d' r  ⇒
    let  r : SNRed [_ ⊢ _] [g' ⊢ M']= r in 
    let r' =
    main_ds [g] [g'] [g' ⊢ M'] [g, x : tm _ ⊢ N1] [g, y : tm _ ⊢ N2] [_ ⊢ σ] rs d' in
    let snr =
    SRCase r [g', x : tm _ ⊢ N1[σ[…], x]] [g', y : tm _ ⊢ N2[σ[…], y]] in
    cr2 [_] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] snr 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