{-# OPTIONS --copatterns --sized-types #-}

module Reduction where

open import Data.Sum
open import Library
open import SizedInfiniteTypes
open import Terms
open import Substitution
open import TermShape
open import SN

data βECxt (Γ : Cxt) : (Δ : Cxt) (a b : Ty)  Set where
  appl  :  {a b} (u : Tm Γ a)                         βECxt Γ Γ (a →̂ b) b
  appr  :  {a b} (t : Tm Γ (a →̂  b))                  βECxt Γ Γ a b
  pairl :  {a b} (u : Tm Γ b)                         βECxt Γ Γ a (a ×̂ b)
  pairr :  {a b} (t : Tm Γ a)                         βECxt Γ Γ b (a ×̂ b)
  fst   :  {a b}                                      βECxt Γ Γ (a ×̂ b) a
  snd   :  {a b}                                      βECxt Γ Γ (a ×̂ b) b
  _∗l   :  {a b∞} (u : Tm Γ ( a))                    βECxt Γ Γ (▸̂ (delay a  b∞)) (▸̂ b∞)
  ∗r_   : ∀{a : Ty}{b∞} (t : Tm Γ (▸̂ (delay a  b∞)))  βECxt Γ Γ ( a) (▸̂ b∞)
  abs   :  {a b}                                      βECxt Γ (a  Γ) b (a →̂  b)
  ▹_    :  {a∞}                                       βECxt Γ Γ (force a∞) (▸̂  a∞)

data βEhole {Γ : Cxt} : {Δ : Cxt} {b a : Ty}  Tm Γ b  βECxt Γ Δ a b  Tm Δ a  Set where
  appl  :  {a b t} (u : Tm Γ a)                           βEhole (app t u) (appl u) (t  (a →̂ b))
  appr  :  {a b u} (t : Tm Γ (a →̂  b))                    βEhole (app t u) (appr t) u
  pairl :  {a b}{t} (u : Tm Γ b)                          βEhole (pair t u) (pairl u) (t  a)
  pairr :  {a b}{u} (t : Tm Γ a)                          βEhole (pair t u) (pairr t) (u  b)
  fst   :  {a b t}                                        βEhole {a = a ×̂ b} (fst t) fst t
  snd   :  {a b t}                                        βEhole {a = a ×̂ b} (snd t) snd t
  _∗l   :  {a b∞ t} (u : Tm Γ ( a))                      βEhole {a = (▸̂ (delay a  b∞))} (t  u) (u ∗l) t
  ∗r_   :  {a : Ty}{b∞}{u} (t : Tm Γ (▸̂ (delay a  b∞)))  βEhole ((t  (u   a))  ▸̂ b∞) (∗r t) u
  abs   :  {a b} {t : Tm (a  Γ) b}                       βEhole (abs t) abs t
  ▹_    :  {a∞} {t : Tm Γ (force a∞)}                     βEhole (▹_ {a∞ = a∞} t) ▹_ t


mkHole :  {Γ Δ} {a b} (E : βECxt Γ Δ a b) {t}  Σ _ \ E[t]  βEhole E[t] E t
mkHole (appl u)  = _ , appl u
mkHole (appr t)  = _ , appr t
mkHole (pairl u) = _ , pairl u
mkHole (pairr t) = _ , pairr t
mkHole fst       = _ , fst
mkHole snd       = _ , snd
mkHole (u ∗l)    = _ , u ∗l
mkHole (∗r t)    = _ , ∗r t
mkHole abs       = _ , abs
mkHole ▹_        = _ , ▹_

data _⇒β_ {Γ} :  {a}  Tm Γ a  Tm Γ a  Set where

  β     :  {a b}{t : Tm (a  Γ) b}{u}
           (app (abs t) u) ⇒β subst0 u t

  β▹    :  {a b∞}{t : Tm Γ (a →̂  force b∞)}{u : Tm Γ a}
            ( t   u) ⇒β (▹_ {a∞ = b∞} (app t u))

  βfst  :  {a b}{t : Tm Γ a}{u : Tm Γ b}
           fst (pair t u) ⇒β t

  βsnd  :  {a b}{t : Tm Γ a}{u : Tm Γ b}
           snd (pair t u) ⇒β u

  cong  :  {Δ a b t t' Et Et'}{E : βECxt Γ Δ a b}
           (𝑬𝒕 : βEhole Et E t)
           (𝑬𝒕' : βEhole Et' E t')
           (t⇒β : t ⇒β t')
           Et ⇒β Et'


subst⇒β :  {m vt a Γ} {t t' : Tm Γ a} {Δ}
           (σ : RenSub {m} vt Γ Δ)  t ⇒β t'  subst σ t ⇒β subst σ t'
subst⇒β σ (β {t = t} {u = u})            = ≡.subst  t'  app (abs (subst (lifts σ) t)) (subst σ u) ⇒β t')
                                                   (sgs-lifts-term {σ = σ} {u} {t})
                                           β
subst⇒β σ β▹                             = β▹
subst⇒β σ βfst                           = βfst
subst⇒β σ βsnd                           = βsnd
subst⇒β σ (cong (appl u) (appl .u) t⇒)   = cong (appl _) (appl _) (subst⇒β σ t⇒)
subst⇒β σ (cong (appr t₁) (appr .t₁) t⇒) = cong (appr _) (appr _) (subst⇒β σ t⇒)
subst⇒β σ (cong fst fst t⇒)              = cong fst fst (subst⇒β σ t⇒)
subst⇒β σ (cong snd snd t⇒)              = cong snd snd (subst⇒β σ t⇒)
subst⇒β σ (cong (u ∗l) (.u ∗l) t⇒)       = cong (_ ∗l) (_ ∗l) (subst⇒β σ t⇒)
subst⇒β σ (cong (∗r t₁) (∗r .t₁) t⇒)     = cong (∗r _) (∗r _) (subst⇒β σ t⇒)
subst⇒β σ (cong abs abs t⇒)              = cong abs abs (subst⇒β (lifts σ) t⇒)
subst⇒β σ (cong ▹_ ▹_ t⇒)                = cong ▹_ ▹_ (subst⇒β σ t⇒)
subst⇒β σ (cong (pairr t) (pairr ._) t⇒) = cong (pairr (subst σ t)) (pairr _) (subst⇒β σ t⇒)
subst⇒β σ (cong (pairl u) (pairl ._) t⇒) = cong (pairl (subst σ u)) (pairl _) (subst⇒β σ t⇒)

data _⇒β*_ {Γ} {a} : Tm Γ a  Tm Γ a  Set where
  []  :  {t}  t ⇒β* t
  _∷_ :  {ti tm to}  ti ⇒β tm  tm ⇒β* to  ti ⇒β* to

_++β_ :  {Γ} {a} {t₀ t₁ t₂ : Tm Γ a}  t₀ ⇒β* t₁  t₁ ⇒β* t₂  t₀ ⇒β* t₂
[] ++β ys = ys
(x  xs) ++β ys = x  (xs ++β ys)

cong* :  {a Γ Δ} {b} {t tβ* : Tm Γ a} {E : βECxt Δ Γ a b}{E[t] E[tβ*]}  βEhole E[t] E t  βEhole E[tβ*] E tβ*  t ⇒β* tβ*  E[t] ⇒β* E[tβ*]
cong* (appl u)   (appl .u)   []       = []
cong* (appr t₁)  (appr .t₁)  []       = []
cong* (pairl u)  (pairl .u)  []       = []
cong* (pairr t₁) (pairr .t₁) []       = []
cong* fst        fst         []       = []
cong* snd        snd         []       = []
cong* (u ∗l)     (.u ∗l)     []       = []
cong* (∗r t₁)    (∗r .t₁)    []       = []
cong* abs        abs         []       = []
cong* ▹_         ▹_          []       = []
cong* E1         E2          (x  t⇒) = cong E1 (proj₂ (mkHole _)) x  cong* (proj₂ (mkHole _)) E2 t⇒

mutual
  EC→βEC :  {Γ} {a b} (E : ECxt Γ a b)  βECxt Γ Γ a b 
  EC→βEC (appl u) = appl u
  EC→βEC fst = fst
  EC→βEC snd = snd
  EC→βEC (u ∗l) = u ∗l
  EC→βEC (∗r t) = ∗r ( t)

  mkHole4 :  {Γ} {a b} (E : ECxt Γ a b) {t : Tm Γ a}  βEhole (E [ t ]) (EC→βEC E) t
  mkHole4 (appl u) = appl u
  mkHole4 fst = fst
  mkHole4 snd = snd
  mkHole4 (u ∗l) = u ∗l
  mkHole4 (∗r t) = ∗r ( t)

cong*3 :  {Γ a b t t'}(E : ECxt* Γ a b)
           (t⇒ : t ⇒β t')
           E [ t ]* ⇒β E [ t' ]*
cong*3 [] t⇒ = t⇒
cong*3 (x  E) t⇒ = cong*3 E (cong (mkHole4 x) (mkHole4 x) t⇒)

cong*4 :  {Γ a b t t'}(E : ECxt* Γ a b)
           (t⇒ : t ⇒β* t')
           E [ t ]* ⇒β* E [ t' ]*
cong*4 E [] = []
cong*4 E (x  xs) = cong*3 E x  cong*4 E xs

subst⇒β*₀ :  {m vt a Γ} {t t' : Tm Γ a} {Δ} (σ : RenSub {m} vt Γ Δ)  t ⇒β* t'  subst σ t ⇒β* subst σ t'
subst⇒β*₀ σ [] = []
subst⇒β*₀ σ (x  xs) = (subst⇒β σ x)  (subst⇒β*₀ σ xs)

-- map⇒β : ∀ {m n} → .(m ≤ℕ n) → ∀ {Γ a}{t t' : Tm Γ a} → t ⟨ n ⟩⇒ t' → t ⟨ m ⟩⇒ t'
-- map⇒β m≤n (β t∈SN) = β (mapSN m≤n t∈SN)
-- map⇒β m≤n (β▹ {a = a}) = β▹ {a = a}
-- map⇒β m≤n (βfst t∈SN) = βfst (mapSN m≤n t∈SN)
-- map⇒β m≤n (βsnd t∈SN) = βsnd (mapSN m≤n t∈SN)
-- map⇒β m≤n (cong Et Et' t→t') = cong Et Et' (map⇒ m≤n t→t')

mutual
  subst⇒β* :  {m vt a Γ} {Δ} {σ ρ : RenSub {m} vt Γ Δ}  (∀ {b} (x : Var Γ b)  vt2tm _ (σ x) ⇒β* vt2tm _ (ρ x))
              (t : Tm Γ a)  subst σ t ⇒β* subst ρ t
  subst⇒β* σ₁ (var x) = σ₁ x
  subst⇒β* {vt = vt} σ₁ (abs t) = cong* abs abs (subst⇒β* (lifts⇒β* {vt = vt} σ₁) t)
  subst⇒β* σ₁ (app t t₁) = cong* (appl _) (appl _) (subst⇒β* σ₁ t) ++β cong* (appr _) (appr _) (subst⇒β* σ₁ t₁)
  subst⇒β* σ₁ (pair t t₁) = cong* (pairl _) (pairl _) (subst⇒β* σ₁ t) ++β
                              cong* (pairr _) (pairr _) (subst⇒β* σ₁ t₁)
  subst⇒β* σ₁ (fst t) = cong* fst fst (subst⇒β* σ₁ t)
  subst⇒β* σ₁ (snd t) = cong* snd snd (subst⇒β* σ₁ t)
  subst⇒β* σ₁ ( t) = cong* ▹_ ▹_ (subst⇒β* σ₁ t)
  subst⇒β* σ₁ (t  t₁) = cong* (_ ∗l) (_ ∗l) (subst⇒β* σ₁ t) ++β
                           cong* (∗r _) (∗r _) (subst⇒β* σ₁ t₁)

  lifts⇒β* :  {m vt a Γ} {Δ} {σ ρ : RenSub {m} vt Γ Δ}  (∀ {b} (x : Var Γ b)  vt2tm _ (σ x) ⇒β* vt2tm _ (ρ x))
               (∀ {b} (x : Var (a  Γ) b)  vt2tm _ (lifts {a = a} σ x) ⇒β* vt2tm _ (lifts {a = a} ρ x))
  lifts⇒β* {vt = `Var} σ₁ (zero) = []
  lifts⇒β* {vt = `Tm}  σ₁ (zero) = []
  lifts⇒β* {vt = `Var} σ₁ (suc x)   = subst⇒β*₀ {vt = `Var} suc (σ₁ x)
  lifts⇒β* {vt = `Tm}  σ₁ (suc x)   = subst⇒β*₀ {vt = `Var} suc (σ₁ x)

mutual
  beta-shr :  {i n a Γ} {t  th : Tm Γ a}  t ⇒β   i size t  n ⟩⇒ th  (  th)  Σ _ \ t'  i size   n ⟩⇒ t' × th ⇒β* t'
  beta-shr β (β 𝒖)                                                   = inj₁ ≡.refl
  beta-shr (cong (appl u) (appl .u) (cong abs abs tβ⇒)) (β 𝒖)        = inj₂ (_ , β 𝒖 , (subst⇒β (sgs u) tβ⇒  []))
  beta-shr (cong (appr ._) (appr ._) tβ⇒) (β {t = t} 𝒖)
    = inj₂ (_ , β (mapβSN tβ⇒ 𝒖) , subst⇒β* {vt = `Tm}  { {._} (zero)  tβ⇒  [] ; (suc x)  [] }) t)
  beta-shr β▹ β▹                                                     = inj₁ ≡.refl
  beta-shr (cong (._ ∗l) (._ ∗l) (cong ▹_ ▹_ tβ⇒)) β▹                = inj₂ (_ , β▹ , cong ▹_ ▹_ (cong (appl _) (appl _) tβ⇒)  [])
  beta-shr (cong (∗r ._) (∗r ._) (cong ▹_ ▹_ tβ⇒)) β▹                = inj₂ (_ , β▹ , cong ▹_ ▹_ (cong (appr _) (appr _) tβ⇒)  [])
  beta-shr βfst (βfst 𝒖)                                             = inj₁ ≡.refl
  beta-shr (cong fst fst (cong (pairl u) (pairl .u) tβ⇒)) (βfst 𝒖)   = inj₂ (_ , ((βfst 𝒖) , (tβ⇒  [])))
  beta-shr (cong fst fst (cong (pairr th) (pairr .th) tβ⇒)) (βfst 𝒖) = inj₂ (_ , βfst (mapβSN tβ⇒ 𝒖) , [])
  beta-shr (cong snd snd (cong (pairl u) (pairl .u) tβ⇒)) (βsnd 𝒖)   = inj₂ (_ , βsnd (mapβSN tβ⇒ 𝒖) , [])
  beta-shr (cong snd snd (cong (pairr th) (pairr .th) tβ⇒)) (βsnd 𝒖) = inj₂ (_ , ((βsnd 𝒖) , (tβ⇒  [])))
  beta-shr βsnd (βsnd 𝒖)                                             = inj₁ ≡.refl
  beta-shr β (cong (appl u) (appl .u) (cong () 𝑬𝒕' th⇒))
  beta-shr β▹ (cong (._ ∗l) (._ ∗l) (cong () 𝑬𝒕' th⇒))
  beta-shr β▹ (cong (∗r t) (∗r .t) (cong () 𝑬𝒕' th⇒))
  beta-shr βfst (cong fst fst (cong () 𝑬𝒕' th⇒))
  beta-shr βsnd (cong snd snd (cong () 𝑬𝒕' th⇒))
  beta-shr (cong E1 E2 t⇒) (cong E0 E3 th⇒)                          = helper E1 E2 t⇒ E0 E3 th⇒

    where
         -- helper : ∀ {i}{j : Size< i}{n a Γ} {t tβ th : Tm Γ a} {Δ a₁} {t₁ ta : Tm Δ a₁}
         --   {E : βECxt Γ Δ a₁ a} {a₂} {t₂ tb : Tm Γ a₂} {E₁ : ECxt Γ a₂ a} →
         -- βEhole t E t₁ →
         -- βEhole tβ E ta →
         -- t₁ ⇒β ta →
         -- Ehole t E₁ t₂ →
         -- Ehole th E₁ tb →
         -- j size t₂ ⟨ n ⟩⇒ tb →
         -- tβ ≡ th ⊎
         -- Σ (Tm Γ a) (λ tm → Σ (i size tβ ⟨ n ⟩⇒ tm) (λ x → th ⇒β* tm))
      helper :  {i}{n a Γ} {t  th : Tm Γ a} {Δ a₁} {t₁ ta : Tm Δ a₁}
           {E : βECxt Γ Δ a₁ a} {a₂} {t₂ tb : Tm Γ a₂} {E₁ : ECxt Γ a₂ a} 
         βEhole t E t₁ 
         βEhole  E ta 
         t₁ ⇒β ta 
         Ehole t E₁ t₂ 
         Ehole th E₁ tb 
         i size t₂  n ⟩⇒ tb 
           th 
         Σ (Tm Γ a)  tm  Σ (i size   n ⟩⇒ tm)  x  th ⇒β* tm))
      helper (appl u) (appl .u) t⇒₁ (appl .u) (appl .u) th⇒₁ with beta-shr t⇒₁ th⇒₁
      helper (appl u) (appl .u) t⇒₁ (appl .u) (appl .u) th⇒₁ | inj₁ ≡.refl = inj₁ ≡.refl
      helper (appl u) (appl .u) t⇒₁ (appl .u) (appl .u) th⇒₁ | inj₂ (tm , h⇒tm , tm⇒β)
             = inj₂ (_ , cong (appl _) (appl _) h⇒tm , cong* (appl _) (appl _) tm⇒β)
      helper (appr t₂) (appr .t₂) t⇒₁ (appl t₁) (appl .t₁) th⇒₁ = inj₂ (_ , cong (appl _) (appl _) th⇒₁ , (cong (appr _) (appr _) t⇒₁  []))
      helper fst fst t⇒₁ fst fst th⇒₁ with beta-shr t⇒₁ th⇒₁
      helper fst fst t⇒₁ fst fst th⇒₁ | inj₁ x = inj₁ (≡.cong fst x)
      helper fst fst t⇒₁ fst fst th⇒₁ | inj₂ (tm , h⇒tm , tm⇒β) = inj₂ (_ , ((cong fst fst h⇒tm) , cong* fst fst tm⇒β))
      helper snd snd t⇒₁ snd snd th⇒₁ with beta-shr t⇒₁ th⇒₁
      helper snd snd t⇒₁ snd snd th⇒₁ | inj₁ x = inj₁ (≡.cong snd x)
      helper snd snd t⇒₁ snd snd th⇒₁ | inj₂ (tm , h⇒tm , tm⇒β) = inj₂ (_ , ((cong snd snd h⇒tm) , cong* snd snd tm⇒β))
      helper (u ∗l) (.u ∗l) t⇒₁ (.u ∗l) (.u ∗l) th⇒₁ with beta-shr t⇒₁ th⇒₁
      helper (u ∗l) (.u ∗l) t⇒₁ (.u ∗l) (.u ∗l) th⇒₁ | inj₁ ≡.refl = inj₁ ≡.refl
      helper (u ∗l) (.u ∗l) t⇒₁ (.u ∗l) (.u ∗l) th⇒₁ | inj₂ (tm , h⇒tm , tm⇒β) = inj₂ (_ , ((cong (_ ∗l) (_ ∗l) h⇒tm) , (cong* (_ ∗l) (_ ∗l) tm⇒β)))
      helper (∗r t₂) (∗r .t₂) t⇒₁ (t₁ ∗l) (.t₁ ∗l) th⇒₁ = inj₂ (_ , ((cong (_ ∗l) (_ ∗l) th⇒₁) , (cong (∗r _) (∗r _) t⇒₁  [])))
      helper (t₂ ∗l) (.t₂ ∗l) (cong ▹_ ▹_ t⇒₁) (∗r t) (∗r .t) th⇒₁
            = inj₂ (_ , ((cong (∗r _) (∗r _) th⇒₁) , (cong (_ ∗l) (_ ∗l) (cong ▹_ ▹_ t⇒₁)  [])))
      helper (∗r .( t)) (∗r .( t)) t⇒₁ (∗r t) (∗r .t) th⇒₁ with beta-shr t⇒₁ th⇒₁
      ... | inj₁ ≡.refl = inj₁ ≡.refl
      ... | inj₂ (tm , h⇒tm , tm⇒β) = inj₂ (_ , ((cong (∗r _) (∗r _) h⇒tm) , cong* (∗r _) (∗r _) tm⇒β))

  mapβSNe :  {i n a Γ} {t t' : Tm Γ a}  t ⇒β t'  SNe {i} n t  SNe {i} n t'
  mapβSNe β                                     (elim (elim 𝒏 ()) (appl 𝒖))
  mapβSNe β▹                                    (elim (elim 𝒏 ()) (𝒖 ∗l))
  mapβSNe β▹                                    (elim (elim 𝒏 ()) (∗r 𝒕))
  mapβSNe βfst                                  (elim (elim 𝒏 ()) fst)
  mapβSNe βsnd                                  (elim (elim 𝒏 ()) snd)
  mapβSNe (cong (appl u) (appl .u) t⇒)          (elim 𝒏 (appl 𝒖))   = elim (mapβSNe t⇒ 𝒏) (appl 𝒖)
  mapβSNe (cong (appr t₁) (appr .t₁) t⇒)        (elim 𝒏 (appl 𝒖))   = elim 𝒏 (appl (mapβSN t⇒ 𝒖))
  mapβSNe (cong fst fst t⇒)                     (elim  𝒏 fst)        = elim  (mapβSNe t⇒ 𝒏) fst
  mapβSNe (cong snd snd t⇒)                     (elim  𝒏 snd)        = elim  (mapβSNe t⇒ 𝒏) snd
  mapβSNe (cong (u ∗l) (.u ∗l) t⇒)              (elim  𝒏 (𝒖 ∗l))     = elim  (mapβSNe t⇒ 𝒏) (𝒖 ∗l)
  mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim 𝒏 (∗r ne (elim _ ())))
  mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim  𝒏 (∗r ▹0))    = elim  𝒏 (∗r_ ▹0)
  mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim  𝒏 (∗r ( 𝒕))) = elim  𝒏 (∗r ( mapβSN t⇒ 𝒕))
  mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim 𝒏 (∗r exp (cong () 𝑬𝒕' t⇒₁) 𝒕))
  mapβSNe (cong (∗r t₁) (∗r .t₁) t⇒)            (elim  𝒏 (_∗l 𝒖))     = elim  𝒏 (mapβSN t⇒ 𝒖 ∗l)
  mapβSNe (cong (∗r ._) (∗r ._) t⇒)             (elim  𝒏 (∗r 𝒕))     = elim  (mapβSNe t⇒ 𝒏) (∗r 𝒕)
  -- mapβSNe (cong fst fst t⇒)                     (elim {j₁ = j₁} {j₂ = j₂} 𝒏 fst)        = elim {j₁ = j₁} {j₂ = j₂} (mapβSNe t⇒ 𝒏) fst
  -- mapβSNe (cong snd snd t⇒)                     (elim {j₁ = j₁} {j₂ = j₂} 𝒏 snd)        = elim {j₁ = j₁} {j₂ = j₂} (mapβSNe t⇒ 𝒏) snd
  -- mapβSNe (cong (u ∗l) (.u ∗l) t⇒)              (elim {j₁ = j₁} {j₂ = j₂} 𝒏 (𝒖 ∗l))     = elim {j₁ = j₁} {j₂ = j₂} (mapβSNe t⇒ 𝒏) (𝒖 ∗l)
  -- mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim 𝒏 (∗r ne (elim _ ())))
  -- mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim {j₁ = j₁} {j₂ = j₂} 𝒏 (∗r ▹0))    = elim {j₁ = j₁} {j₂ = j₂} 𝒏 (∗r_ ▹0)
  -- mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim {j₁ = j₁} {j₂ = j₂} 𝒏 (∗r (▹ 𝒕))) = elim {j₁ = j₁} {j₂ = j₂} 𝒏 (∗r (▹ mapβSN t⇒ 𝒕))
  -- mapβSNe (cong (u ∗l) (.u ∗l) (cong ▹_ ▹_ t⇒)) (elim 𝒏 (∗r exp (cong () 𝑬𝒕' t⇒₁) 𝒕))
  -- mapβSNe (cong (∗r t₁) (∗r .t₁) t⇒)            (elim {j₁ = j₁} {j₂ = j₂} 𝒏 (_∗l 𝒖))     = elim {j₁ = j₁} {j₂ = j₂} 𝒏 (mapβSN t⇒ 𝒖 ∗l)
  -- mapβSNe (cong (∗r ._) (∗r ._) t⇒)             (elim {j₁ = j₁} {j₂ = j₂} 𝒏 (∗r 𝒕))     = elim {j₁ = j₁} {j₂ = j₂} (mapβSNe t⇒ 𝒏) (∗r 𝒕)
  mapβSNe (cong abs abs t⇒)                     (elim 𝒏 ())
  mapβSNe (cong ▹_ ▹_ t⇒)                       (elim 𝒏 ())
  mapβSNe (cong (pairr _) (pairr ._) t⇒)        (elim 𝒏 ())
  mapβSNe (cong (pairl _) (pairl ._) t⇒)        (elim 𝒏 ())

  mapβSN :  {i n a Γ} {t t' : Tm Γ a}  t ⇒β t'  SN {i} n t  SN {i} n t'
  mapβSN t⇒                (ne 𝒏)                      = ne (mapβSNe t⇒ 𝒏)
  mapβSN (cong abs abs t⇒) (abs 𝒕)                     = abs (mapβSN t⇒ 𝒕)
  mapβSN (cong (pairl u)   (pairl .u) t⇒) (pair 𝒕 𝒕₁)  = pair (mapβSN t⇒ 𝒕) 𝒕₁
  mapβSN (cong (pairr t₁)  (pairr .t₁) t⇒) (pair 𝒕 𝒕₁) = pair 𝒕 (mapβSN t⇒ 𝒕₁)
  mapβSN (cong ▹_ ▹_ t⇒)   ▹0                          = ▹0
  mapβSN (cong ▹_ ▹_ t⇒)   ( 𝒕)                       =  mapβSN t⇒ 𝒕
  mapβSN t⇒                (exp t⇒₁ 𝒕)                 with beta-shr t⇒ t⇒₁
  mapβSN t⇒ (exp t⇒₁ 𝒕) | inj₁ ≡.refl = 𝒕
  mapβSN t⇒ (exp t⇒₁ 𝒕) | inj₂ (_ , t⇒h , t⇒β*) = exp t⇒h (mapβ*SN t⇒β* 𝒕)

  mapβ*SN :  {i n a Γ} {t t' : Tm Γ a}  t ⇒β* t'  SN {i} n t  SN {i} n t'
  mapβ*SN []          𝒕 = 𝒕
  mapβ*SN (t⇒  t⇒β*) 𝒕 = mapβ*SN t⇒β* (mapβSN t⇒ 𝒕)