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;

To download the code: prop_sn_1a.bel