{-# OPTIONS --without-K --safe #-}

module NonCumulative.Statics.Ascribed.Presup where

open import Lib
open import NonCumulative.Statics.Ascribed.Full
open import NonCumulative.Statics.Ascribed.PER
open import NonCumulative.Statics.Ascribed.Refl
open import NonCumulative.Statics.Ascribed.Misc
open import NonCumulative.Statics.Ascribed.CtxEquiv
open import NonCumulative.Statics.Ascribed.Properties.Contexts
open import NonCumulative.Statics.Ascribed.Properties.Subst

mutual
  presup-tm :  {i} 
              Γ  t ∶[ i ] T 
              ----------------------
               Γ × Γ  T ∶[ 1 + i ] Se i
  presup-tm (N-wf ⊢Γ)        = ⊢Γ , Se-wf zero ⊢Γ
  presup-tm (Se-wf i ⊢Γ)     = ⊢Γ , Se-wf (suc i) ⊢Γ
  presup-tm (Liftt-wf n ⊢T)
    with presup-tm ⊢T
  ...  | ⊢Γ , _              = ⊢Γ , Se-wf (n + _) ⊢Γ
  presup-tm (Π-wf ⊢S ⊢T eq)
    with presup-tm ⊢S
  ...  | ⊢Γ , _              = ⊢Γ , Se-wf _ ⊢Γ
  presup-tm (vlookup ⊢Γ T∈Γ) = ⊢Γ , ∈⇒ty-wf ⊢Γ T∈Γ
  presup-tm (ze-I ⊢Γ)        = ⊢Γ , N-wf ⊢Γ
  presup-tm (su-I ⊢t)        = presup-tm ⊢t
  presup-tm (N-E ⊢T ⊢s ⊢r ⊢t)
    with presup-tm ⊢T
  ... | ⊢∷ ⊢Γ _ , _          = ⊢Γ , t[σ]-Se ⊢T (⊢I,t ⊢Γ (N-wf ⊢Γ) ⊢t)
  presup-tm (Λ-I ⊢S ⊢t eq)
    with presup-tm ⊢t
  ...  | ⊢∷ ⊢Γ _ , ⊢T        = ⊢Γ , Π-wf ⊢S ⊢T eq
  presup-tm (Λ-E ⊢S ⊢T ⊢t ⊢s eq)
    with presup-tm ⊢S
  ...  | ⊢Γ , _              = ⊢Γ , t[σ]-Se ⊢T (⊢I,t ⊢Γ ⊢S ⊢s)
  presup-tm (L-I n ⊢t)
    with presup-tm ⊢t
  ...  | ⊢Γ , ⊢T             = ⊢Γ , Liftt-wf n ⊢T
  presup-tm (L-E n ⊢T ⊢t)    = proj₁ (presup-tm ⊢T) , ⊢T
  presup-tm (t[σ] ⊢t ⊢σ)
    with presup-tm ⊢t | presup-s ⊢σ
  ...  | _ , ⊢T | ⊢Γ , _     = ⊢Γ , t[σ]-Se ⊢T ⊢σ
  presup-tm (conv ⊢t S≈T)
    with presup-≈ S≈T
  ...  | ⊢Γ , _ , ⊢T , _     = ⊢Γ , ⊢T

  presup-s : Γ ⊢s σ  Δ 
             ------------
              Γ ×  Δ
  presup-s (s-I ⊢Γ)             = ⊢Γ , ⊢Γ
  presup-s (s-wk ⊢TΓ@(⊢∷ ⊢Γ _)) = ⊢TΓ , ⊢Γ
  presup-s (s-∘ ⊢σ ⊢δ)          = proj₁ (presup-s ⊢σ) , proj₂ (presup-s ⊢δ)
  presup-s (s-, ⊢σ ⊢T ⊢t)
    with ⊢Γ , ⊢Δpresup-s ⊢σ  = ⊢Γ , ⊢∷ ⊢Δ ⊢T
  presup-s (s-conv ⊢σ Δ′≈Δ)     = proj₁ (presup-s ⊢σ) , proj₂ (presup-⊢≈ Δ′≈Δ)


  presup-≈ :  {i} 
             Γ  s  t ∶[ i ] T 
             -----------------------------------
              Γ × Γ  s ∶[ i ] T × Γ  t ∶[ i ] T × Γ  T ∶[ 1 + i ] Se i
  presup-≈ (N-[] ⊢σ)
    with presup-s ⊢σ
  ...  | ⊢Γ , ⊢Δ                           = ⊢Γ , t[σ]-Se (N-wf ⊢Δ) ⊢σ , N-wf ⊢Γ , Se-wf zero ⊢Γ
  presup-≈ (Se-[] i ⊢σ)
    with presup-s ⊢σ
  ...  | ⊢Γ , ⊢Δ                           = ⊢Γ , t[σ]-Se (Se-wf i ⊢Δ) ⊢σ , Se-wf i ⊢Γ , Se-wf (suc i) ⊢Γ
  presup-≈ (Liftt-[] n ⊢σ ⊢T)
    with presup-s ⊢σ
  ...  | ⊢Γ , ⊢Δ                           = ⊢Γ , t[σ]-Se (Liftt-wf n ⊢T) ⊢σ , Liftt-wf n (t[σ]-Se ⊢T ⊢σ) , Se-wf (n + _) ⊢Γ
  presup-≈ (Π-[] ⊢σ ⊢S ⊢T eq)
    with presup-s ⊢σ
  ...  | ⊢Γ , ⊢Δ                           = ⊢Γ , t[σ]-Se (Π-wf ⊢S ⊢T eq) ⊢σ , Π-wf (t[σ]-Se ⊢S ⊢σ) (t[σ]-Se ⊢T (⊢q ⊢Γ ⊢σ ⊢S)) eq , Se-wf _ ⊢Γ
  presup-≈ (Π-cong ⊢S S≈S′ T≈T′ eq)
    with presup-≈ S≈S′ | presup-≈ T≈T′
  ...  | ⊢Γ , ⊢S , ⊢S′ , _
       | _ , ⊢T , ⊢T′ , _                  = ⊢Γ , Π-wf ⊢S ⊢T eq , Π-wf ⊢S′ (ctxeq-tm (∷-cong (≈-Ctx-refl ⊢Γ) ⊢S ⊢S′ S≈S′ S≈S′) ⊢T′) eq , Se-wf _ ⊢Γ
  presup-≈ (Liftt-cong n T≈T′)
    with presup-≈ T≈T′
  ...  | ⊢Γ , ⊢T , ⊢T′ , _                 = ⊢Γ , Liftt-wf n ⊢T , Liftt-wf n ⊢T′ , Se-wf (n + _) ⊢Γ
  presup-≈ (v-≈ ⊢Γ T∈Γ)                    = ⊢Γ , vlookup ⊢Γ T∈Γ , vlookup ⊢Γ T∈Γ , ∈⇒ty-wf ⊢Γ T∈Γ
  presup-≈ (ze-≈ ⊢Γ)                       = ⊢Γ , ze-I ⊢Γ , ze-I ⊢Γ , N-wf ⊢Γ
  presup-≈ (su-cong t≈t′)
    with presup-≈ t≈t′
  ...  | ⊢Γ , ⊢t , ⊢t′ , ⊢N                 = ⊢Γ , su-I ⊢t , su-I ⊢t′ , ⊢N
  presup-≈ (rec-cong ⊢T T≈T′ s≈s′ r≈r′ t≈t′)
    with ⊢NΓ , ⊢T , ⊢T′ , _presup-≈ T≈T′
       | ⊢Γ , ⊢s , ⊢s′ , _presup-≈ s≈s′
       | ⊢TNΓ , ⊢r , ⊢r′ , _presup-≈ r≈r′
       | _ , ⊢t , ⊢t′ , _presup-≈ t≈t′    = ⊢Γ
                                             , N-E ⊢T ⊢s ⊢r ⊢t
                                             , conv
                                               (N-E ⊢T′ (conv ⊢s′ ([]-cong-Se′ T≈T′ (⊢I,ze ⊢Γ))) (ctxeq-tm (∷-cong′ ⊢NΓ ⊢T ⊢T′ T≈T′) (conv ⊢r′ ([]-cong-Se′ T≈T′ (⊢[wk∘wk],su[v1] ⊢TNΓ)))) ⊢t′)
                                               (≈-sym ([]-cong-Se T≈T′ (⊢I,t ⊢Γ (N-wf ⊢Γ) ⊢t) (,-cong (I-≈ ⊢Γ) (N-wf ⊢Γ) (≈-refl (N-wf ⊢Γ)) (≈-conv-N-[]-sym t≈t′ (s-I ⊢Γ)))))
                                             , (t[σ]-Se ⊢T (⊢I,t ⊢Γ (N-wf ⊢Γ) ⊢t))
  presup-≈ (Λ-cong ⊢S S≈S′ t≈t′ eq)
    with _ , _ , ⊢S′ , _presup-≈ S≈S′
       | ⊢∷ ⊢Γ _ , ⊢t , ⊢t′ , ⊢Tpresup-≈ t≈t′ = ⊢Γ , Λ-I ⊢S ⊢t eq , conv (Λ-I ⊢S′ (ctxeq-tm (∷-cong (≈-Ctx-refl ⊢Γ) ⊢S ⊢S′ S≈S′ S≈S′) ⊢t′) eq) (≈-sym (Π-cong ⊢S S≈S′ (≈-refl ⊢T) eq)) , Π-wf ⊢S ⊢T eq
  presup-≈ ($-cong ⊢S ⊢T r≈r′ s≈s′ eq)
    with ⊢Γ , ⊢r , ⊢r′ , ⊢ΠSTpresup-≈ r≈r′
       | _ , ⊢s , ⊢s′ , _presup-≈ s≈s′        = ⊢Γ
                                                 , Λ-E ⊢S ⊢T ⊢r ⊢s eq
                                                 , conv (Λ-E ⊢S ⊢T ⊢r′ ⊢s′ eq) ([]-cong-Se″ ⊢T (⊢I,t ⊢Γ ⊢S ⊢s′) (,-cong (I-≈ ⊢Γ) ⊢S (≈-refl ⊢S) (≈-conv (≈-sym s≈s′) (≈-sym ([I] ⊢S)))))
                                                 , t[σ]-Se ⊢T (⊢I,t ⊢Γ ⊢S ⊢s)
  presup-≈ ([]-cong t≈t′ σ≈σ′)
    with _ , ⊢t , ⊢t′ , ⊢Tpresup-≈ t≈t′
       | ⊢Γ , ⊢σ , ⊢σ′ , _presup-s-≈ σ≈σ′     = ⊢Γ , t[σ] ⊢t ⊢σ , conv (t[σ] ⊢t′ ⊢σ′) ([]-cong-Se″ ⊢T ⊢σ′ (s-≈-sym σ≈σ′)) , t[σ]-Se ⊢T ⊢σ
  presup-≈ (liftt-cong n t≈t′)
    with ⊢Γ , ⊢t , ⊢t′ , ⊢Tpresup-≈ t≈t′      = ⊢Γ , L-I n ⊢t , L-I n ⊢t′ , Liftt-wf n ⊢T
  presup-≈ (unlift-cong n ⊢T t≈t′)
    with ⊢Γ , ⊢t , ⊢t′ , _presup-≈ t≈t′       = ⊢Γ , L-E n ⊢T ⊢t , L-E n ⊢T ⊢t′ , ⊢T
  presup-≈ (ze-[] ⊢σ)
    with ⊢Γ , ⊢Δpresup-s ⊢σ    = ⊢Γ , t[σ]-N (ze-I ⊢Δ) ⊢σ , ze-I ⊢Γ , N-wf ⊢Γ
  presup-≈ (su-[] ⊢σ ⊢t)
    with ⊢Γproj₁ (presup-s ⊢σ) = ⊢Γ , t[σ]-N (su-I ⊢t) ⊢σ , su-I (t[σ]-N ⊢t ⊢σ) , N-wf ⊢Γ
  presup-≈ (rec-[] {Γ = Γ} {σ = σ} {Δ = Δ} {T = T} {t = t} {i = i} ⊢σ ⊢T ⊢s ⊢r ⊢t)
    with ⊢Γ , ⊢Δpresup-s ⊢σ = ⊢Γ
                               , conv
                                   (t[σ] (N-E ⊢T ⊢s ⊢r ⊢t) ⊢σ)
                                   (ER.begin
                                      T [| t  N₀ ] [ σ ]
                                    ER.≈⟨ [∘]-Se ⊢T (⊢I,t ⊢Δ (N-wf ⊢Δ) ⊢t) ⊢σ 
                                      T [ (I , t  N₀)  σ ]
                                    ER.≈⟨ []-cong-Se″ ⊢T (s-∘ ⊢σ (⊢I,t ⊢Δ (N-wf ⊢Δ) ⊢t)) ([I,t]∘σ≈σ,t[σ] ⊢NΔ ⊢σ ⊢t) 
                                      T [ σ , sub t σ  N₀ ]
                                    ER.∎)
                               , conv
                                   (N-E ⊢T[qσ]
                                     (conv
                                       (t[σ] ⊢s ⊢σ)
                                       (ER.begin
                                          T [| ze  N₀ ] [ σ ]
                                        ER.≈⟨ [∘]-Se ⊢T (⊢I,ze ⊢Δ) ⊢σ 
                                          T [ (I , ze  N₀)  σ ]
                                        ER.≈⟨ []-cong-Se″ ⊢T (s-∘ ⊢σ (⊢I,ze ⊢Δ)) ([I,ze]∘σ≈σ,ze ⊢Δ ⊢σ) 
                                          T [ σ , ze  N₀ ]
                                        ER.≈˘⟨ []-cong-Se″ ⊢T (s-∘ (⊢I,ze ⊢Γ) ⊢qσ) (qσ∘[I,ze]≈σ,ze ⊢Γ ⊢Δ ⊢σ) 
                                          T [ q N₀ σ  (I , ze  N₀) ]
                                        ER.≈˘⟨ [∘]-Se ⊢T ⊢qσ (⊢I,t ⊢Γ (N-wf ⊢Γ) (ze-I ⊢Γ)) 
                                          T [ q N₀ σ ] [| ze  N₀ ]
                                        ER.∎))
                                     (conv (t[σ] ⊢r ⊢q[qσ]) (rec-β-su-T-swap ⊢Γ ⊢TNΔ ⊢σ))
                                     (t[σ]-N ⊢t ⊢σ))
                                   (≈-trans
                                     ([∘]-Se ⊢T ⊢qσ (⊢I,t ⊢Γ (N-wf ⊢Γ) (t[σ]-N ⊢t ⊢σ)))
                                     ([]-cong-Se″ ⊢T (s-∘ (⊢I,t ⊢Γ (N-wf ⊢Γ) (t[σ]-N ⊢t ⊢σ)) ⊢qσ) (qσ∘[I,t]≈σ,t-N ⊢Γ ⊢Δ (t[σ]-N ⊢t ⊢σ) ⊢σ)))
                                , t[σ]-Se ⊢T (s-, ⊢σ (N-wf ⊢Δ) (t[σ] ⊢t ⊢σ))
    where
      ⊢qσ = ⊢q-N ⊢Γ ⊢Δ ⊢σ
      ⊢T[qσ] = t[σ]-Se ⊢T ⊢qσ
      ⊢NΓ = ⊢∷ ⊢Γ (N-wf ⊢Γ)
      ⊢q[qσ] = ⊢q ⊢NΓ ⊢qσ ⊢T
      ⊢T[qσ]NΓ = ⊢∷ ⊢NΓ ⊢T[qσ]
      ⊢NΔ = ⊢∷ ⊢Δ (N-wf ⊢Δ)
      ⊢TNΔ = ⊢∷ ⊢NΔ ⊢T
  presup-≈ (Λ-[] ⊢σ ⊢S ⊢t eq)
    with ⊢Γproj₁ (presup-s ⊢σ)
       | ⊢∷ _ ⊢S , ⊢Tpresup-tm ⊢t = ⊢Γ
                                     , t[σ] (Λ-I ⊢S ⊢t eq) ⊢σ
                                     , conv
                                       (Λ-I (t[σ]-Se ⊢S ⊢σ) (t[σ] ⊢t (⊢q ⊢Γ ⊢σ ⊢S)) eq)
                                       (≈-sym (Π-[] ⊢σ ⊢S ⊢T eq))
                                     , t[σ]-Se (Π-wf ⊢S ⊢T eq) ⊢σ
  presup-≈ ($-[] ⊢S ⊢T ⊢σ ⊢r ⊢s eq)
    with ⊢Γ , ⊢Δpresup-s ⊢σ       = ⊢Γ
                                     , conv (t[σ] (Λ-E ⊢S ⊢T ⊢r ⊢s eq) ⊢σ) (≈-trans ([∘]-Se ⊢T (⊢I,t ⊢Δ ⊢S ⊢s) ⊢σ) ([]-cong-Se″ ⊢T (s-∘ ⊢σ (⊢I,t ⊢Δ ⊢S ⊢s)) ([I,t]∘σ≈σ,t[σ] (⊢∷ ⊢Δ ⊢S) ⊢σ ⊢s)))
                                     , conv (Λ-E (t[σ]-Se ⊢S ⊢σ) (t[σ]-Se ⊢T (⊢q ⊢Γ ⊢σ ⊢S)) (conv (t[σ] ⊢r ⊢σ) (Π-[] ⊢σ ⊢S ⊢T eq)) (t[σ] ⊢s ⊢σ) eq)
                                            (≈-trans ([∘]-Se ⊢T (⊢q ⊢Γ ⊢σ ⊢S) (⊢I,t ⊢Γ (t[σ]-Se ⊢S ⊢σ) (t[σ] ⊢s ⊢σ)))
                                                     ([]-cong-Se″ ⊢T (s-∘ (⊢I,t ⊢Γ (t[σ]-Se ⊢S ⊢σ) (t[σ] ⊢s ⊢σ)) (⊢q ⊢Γ ⊢σ ⊢S)) (qσ∘[I,t]≈σ,t ⊢Γ ⊢S ⊢σ (t[σ] ⊢s ⊢σ))))
                                     , t[σ]-Se ⊢T (s-, ⊢σ ⊢S (t[σ] ⊢s ⊢σ))
  presup-≈ (liftt-[] n ⊢σ ⊢T ⊢t)
    with ⊢Γ , _presup-s ⊢σ        = ⊢Γ , t[σ] (L-I n ⊢t) ⊢σ , conv (L-I n (t[σ] ⊢t ⊢σ)) (≈-sym (Liftt-[] n ⊢σ ⊢T)) , t[σ]-Se (Liftt-wf n ⊢T) ⊢σ
  presup-≈ (unlift-[] n ⊢T ⊢σ ⊢t)
    with ⊢Γ , _presup-s ⊢σ        = ⊢Γ , t[σ] (L-E n ⊢T ⊢t) ⊢σ , L-E n (t[σ]-Se ⊢T ⊢σ) (conv (t[σ] ⊢t ⊢σ) (Liftt-[] n ⊢σ ⊢T)) , t[σ]-Se ⊢T ⊢σ
  presup-≈ (rec-β-ze ⊢T ⊢t ⊢r)
    with ⊢Γproj₁ (presup-tm ⊢t) = ⊢Γ , N-E ⊢T ⊢t ⊢r (ze-I ⊢Γ) , ⊢t , t[σ]-Se ⊢T (⊢I,t ⊢Γ (N-wf ⊢Γ) (ze-I ⊢Γ))
  presup-≈ (rec-β-su {Γ = Γ} {T = T} {s = s} {r = r} {t = t} ⊢T ⊢s ⊢r ⊢t)
    with ⊢TNΓ@(⊢∷ ⊢NΓ@(⊢∷ ⊢Γ ⊢N) _)proj₁ (presup-tm ⊢r) = ⊢Γ
                                                           , N-E ⊢T ⊢s ⊢r (su-I ⊢t)
                                                           , conv
                                                             (t[σ] ⊢r ⊢I,t,recTrst)
                                                             (≈-trans ([∘]-Se ⊢T ⊢[wk∘wk],su[v1]′ ⊢I,t,recTrst) ([]-cong-Se″ ⊢T (s-∘ ⊢I,t,recTrst ⊢[wk∘wk],su[v1]′) lemma))
                                                           , t[σ]-Se ⊢T (⊢I,t ⊢Γ ⊢N (su-I ⊢t))
    where
      ⊢recTsrt = N-E ⊢T ⊢s ⊢r ⊢t
      ⊢I,t,recTrst = s-, (⊢I,t ⊢Γ ⊢N ⊢t) ⊢T (N-E ⊢T ⊢s ⊢r ⊢t)
      ⊢wk∘wk = s-∘ (s-wk ⊢TNΓ) (s-wk ⊢NΓ)
      ⊢[wk∘wk],su[v1]′ = s-, ⊢wk∘wk ⊢N (conv-N-[]-sym (su-I (⊢vn∶N L.[ T  _ ] ⊢TNΓ refl)) ⊢wk∘wk)

      lemma : Γ ⊢s ((wk  wk) , su (v 1)  N₀)  ((I , t  N₀) , rec (T  _) s r t  T  _)  I , su t  N₀  N₀  Γ
      lemma =
        begin
          ((wk  wk) , su (v 1)  N₀)  ((I , t  N₀) , rec (T  _) s r t  T  _)
        ≈⟨ ,-∘ ⊢wk∘wk ⊢N (conv-N-[]-sym (su-I (⊢vn∶N L.[ T  _ ] ⊢TNΓ refl)) ⊢wk∘wk) ⊢I,t,recTrst 
          (wk  wk  ((I , t  N₀) , rec (T  _) s r t  T  _)) , su (v 1) [ (I , t  N₀) , rec (T  _) s r t  T  _ ]  N₀
        ≈⟨ ,-cong lemma-l ⊢N (≈-refl ⊢N) (≈-conv-N-[]-sym lemma-r (s-∘ ⊢I,t,recTrst ⊢wk∘wk)) 
          I , su t  N₀
        
        where
          lemma-r : Γ  su (v 1) [ (I , t  N₀) , rec (T  _) s r t  T  _ ]  su t ∶[ 0 ] N
          lemma-r =
            begin
              su (v 1) [ (I , t  N₀) , rec (T  _) s r t  T  _ ]
            ≈⟨ su-[] ⊢I,t,recTrst (⊢vn∶N L.[ T  _ ] ⊢TNΓ refl) 
              su (v 1 [ (I , t  N₀) , rec (T  _) s r t  T  _ ])
            ≈⟨ su-cong (≈-conv ([,]-v-su (⊢I,t ⊢Γ ⊢N ⊢t) ⊢T ⊢recTsrt here) (N-[][] (s-wk ⊢NΓ) (⊢I,t ⊢Γ ⊢N ⊢t))) 
              su (v 0 [ I , t  N₀ ])
            ≈⟨ su-cong (≈-conv-N-[] ([,]-v-ze (s-I ⊢Γ) ⊢N (conv-N-[]-sym ⊢t (s-I ⊢Γ))) (s-I ⊢Γ)) 
              su t
            
            where
              open ER

          open SR

          lemma-l : Γ ⊢s wk  wk  ((I , t  N₀) , rec (T  _) s r t  T  _)  I  Γ
          lemma-l = wk∘wk∘,, ⊢Γ (s-I ⊢Γ) ⊢N ⊢T (conv ⊢t (≈-sym ([I] ⊢N))) ⊢recTsrt

  presup-≈ (Λ-β ⊢S ⊢T ⊢t ⊢s)
    with ⊢∷ ⊢Γ _ , _presup-tm ⊢t       = ⊢Γ , Λ-E ⊢S ⊢T (Λ-I ⊢S ⊢t refl) ⊢s refl , t[σ] ⊢t (⊢I,t ⊢Γ ⊢S ⊢s) , t[σ]-Se ⊢T (⊢I,t ⊢Γ ⊢S ⊢s)
  presup-≈ (Λ-η ⊢S ⊢T ⊢s eq)
    with ⊢Γ , ⊢ΠSTpresup-tm ⊢s         = ⊢Γ , ⊢s
                                          , conv (Λ-I ⊢S (Λ-E ⊢S[wk]
                                                              (t[σ]-Se ⊢T (⊢q ⊢SΓ (s-wk ⊢SΓ) ⊢S))
                                                              (conv (t[σ] ⊢s (s-wk ⊢SΓ)) (Π-[] (s-wk ⊢SΓ) ⊢S ⊢T eq))
                                                              ⊢v0 eq)
                                                         eq)
                                                 (Π-cong ⊢S (≈-refl ⊢S)
                                                         (≈-trans ([∘]-Se ⊢T (⊢q ⊢SΓ (s-wk ⊢SΓ) ⊢S) ⊢I,v0)
                                                         (≈-trans ([]-cong-Se″ ⊢T (s-∘ ⊢I,v0 (⊢q ⊢SΓ (s-wk ⊢SΓ) ⊢S)) (q[wk]∘[I,v0]≈I ⊢SΓ))
                                                                  ([I] ⊢T)))
                                                         eq)
                                          , ⊢ΠST
    where
      ⊢SΓ    = ⊢∷ ⊢Γ ⊢S
      ⊢S[wk] = t[σ]-Se ⊢S (s-wk ⊢SΓ)
      ⊢v0    = vlookup ⊢SΓ here
      ⊢I,v0  = ⊢I,t ⊢SΓ ⊢S[wk] ⊢v0
  presup-≈ (L-β n ⊢t)
    with presup-tm ⊢t
  ...  | ⊢Γ , ⊢T                          = ⊢Γ , L-E n ⊢T (L-I n ⊢t) , ⊢t , ⊢T
  presup-≈ (L-η n ⊢T ⊢t)
    with presup-tm ⊢t
  ...  | ⊢Γ , ⊢LT                         = ⊢Γ , ⊢t , L-I n (L-E n ⊢T ⊢t) , ⊢LT
  presup-≈ ([I] ⊢t)
    with ⊢Γ , ⊢Tpresup-tm ⊢t           = ⊢Γ , conv (t[σ] ⊢t (s-I ⊢Γ)) ([I] ⊢T) , ⊢t , ⊢T
  presup-≈ ([wk] ⊢Γ ⊢S T∈Γ)               = ⊢SΓ , t[σ] (vlookup ⊢Γ T∈Γ) (s-wk ⊢SΓ) , vlookup ⊢SΓ (there T∈Γ) , t[σ]-Se (∈⇒ty-wf ⊢Γ T∈Γ) (s-wk ⊢SΓ)
    where ⊢SΓ = ⊢∷ ⊢Γ ⊢S
  presup-≈ ([∘] ⊢τ ⊢σ ⊢t)
    with ⊢Γproj₁ (presup-s ⊢τ)
       | _ , ⊢Tpresup-tm ⊢t            = ⊢Γ , t[σ] ⊢t (s-∘ ⊢τ ⊢σ) , conv (t[σ] (t[σ] ⊢t ⊢σ) ⊢τ) ([∘]-Se ⊢T ⊢σ ⊢τ) , t[σ]-Se ⊢T (s-∘ ⊢τ ⊢σ)
  presup-≈ ([,]-v-ze ⊢σ ⊢S ⊢t)
    with ⊢Γ , ⊢Δpresup-s ⊢σ            = ⊢Γ
                                          , conv (t[σ] (vlookup ⊢SΔ here) ⊢σ,t) (≈-trans ([∘]-Se ⊢S (s-wk ⊢SΔ) ⊢σ,t) ([]-cong-Se″ ⊢S (s-∘ ⊢σ,t (s-wk ⊢SΔ)) (p-, ⊢σ ⊢S ⊢t)))
                                          , ⊢t , t[σ]-Se ⊢S ⊢σ
    where
      ⊢SΔ  = ⊢∷ ⊢Δ ⊢S
      ⊢σ,t = s-, ⊢σ ⊢S ⊢t
  presup-≈ ([,]-v-su ⊢σ ⊢S ⊢s T∈Δ)
    with ⊢Γ , ⊢Δpresup-s ⊢σ
    with ⊢T∈⇒ty-wf ⊢Δ T∈Δ              = ⊢Γ
                                          , conv (t[σ] (vlookup ⊢SΔ (there T∈Δ)) ⊢σ,s)
                                                 (≈-trans ([∘]-Se ⊢T (s-wk ⊢SΔ) ⊢σ,s) ([]-cong-Se″ ⊢T (s-∘ ⊢σ,s (s-wk ⊢SΔ)) (wk∘[σ,t]≈σ ⊢SΔ ⊢σ ⊢s)))
                                          , t[σ] (vlookup ⊢Δ T∈Δ) ⊢σ , t[σ]-Se ⊢T ⊢σ
    where
      ⊢SΔ  = ⊢∷ ⊢Δ ⊢S
      ⊢σ,s = s-, ⊢σ ⊢S ⊢s
  presup-≈ (≈-conv s≈t S≈T)
    with ⊢Γ , ⊢s , ⊢t , _presup-≈ s≈t
       | _ , _ , ⊢T , _presup-≈ S≈T    = ⊢Γ , conv ⊢s S≈T , conv ⊢t S≈T , ⊢T
  presup-≈ (≈-sym t≈s)
    with ⊢Γ , ⊢t , ⊢s , ⊢Tpresup-≈ t≈s = ⊢Γ , ⊢s , ⊢t , ⊢T
  presup-≈ (≈-trans s≈t′ t′≈t)
    with ⊢Γ , ⊢s , _presup-≈ s≈t′
       | _ , _ , ⊢t , ⊢Tpresup-≈ t′≈t  = ⊢Γ , ⊢s , ⊢t , ⊢T


  presup-s-≈ : Γ ⊢s σ  τ  Δ 
               -----------------------------------
                Γ × Γ ⊢s σ  Δ × Γ ⊢s τ  Δ ×  Δ
  presup-s-≈ (I-≈ ⊢Γ)                          = ⊢Γ , s-I ⊢Γ , s-I ⊢Γ , ⊢Γ
  presup-s-≈ (wk-≈ ⊢TΓ@(⊢∷ ⊢Γ _))              = ⊢TΓ , s-wk ⊢TΓ , s-wk ⊢TΓ , ⊢Γ
  presup-s-≈ (∘-cong σ≈σ′ τ≈τ′)
    with ⊢Γ , ⊢σ , ⊢σ′ , _presup-s-≈ σ≈σ′
       | _  , ⊢τ , ⊢τ′ , ⊢Δpresup-s-≈ τ≈τ′  = ⊢Γ , s-∘ ⊢σ ⊢τ , s-∘ ⊢σ′ ⊢τ′ , ⊢Δ
  presup-s-≈ (,-cong σ≈τ ⊢T T≈T′ t≈t′)
    with ⊢Γ , ⊢σ , ⊢τ , ⊢Δpresup-s-≈ σ≈τ
       | _  , ⊢t , ⊢t′ , _presup-≈ t≈t′
       | _  , _  , ⊢T′ , _presup-≈ T≈T′     = ⊢Γ , s-, ⊢σ ⊢T ⊢t , s-conv (s-, ⊢τ ⊢T′ (conv ⊢t′ ([]-cong-Se T≈T′ ⊢σ σ≈τ))) (∷-cong (≈-Ctx-refl ⊢Δ) ⊢T′ ⊢T (≈-sym T≈T′) (≈-sym T≈T′)) , ⊢∷ ⊢Δ ⊢T
  presup-s-≈ (I-∘ ⊢σ)
    with ⊢Γ , ⊢Δpresup-s ⊢σ                 = ⊢Γ , s-∘ ⊢σ (s-I ⊢Δ) , ⊢σ , ⊢Δ
  presup-s-≈ (∘-I ⊢σ)
    with ⊢Γ , ⊢Δpresup-s ⊢σ                 = ⊢Γ , s-∘ (s-I ⊢Γ) ⊢σ , ⊢σ , ⊢Δ
  presup-s-≈ (∘-assoc ⊢σ ⊢σ′ ⊢σ″)              = proj₁ (presup-s ⊢σ″) , s-∘ ⊢σ″ (s-∘ ⊢σ′ ⊢σ) , s-∘ (s-∘ ⊢σ″ ⊢σ′) ⊢σ , proj₂ (presup-s ⊢σ)
  presup-s-≈ (,-∘ ⊢σ ⊢T ⊢t ⊢τ)                 = proj₁ (presup-s ⊢τ) , s-∘ ⊢τ (s-, ⊢σ ⊢T ⊢t) , s-, (s-∘ ⊢τ ⊢σ) ⊢T (conv (t[σ] ⊢t ⊢τ) ([∘]-Se ⊢T ⊢σ ⊢τ)) , ⊢∷ (proj₂ (presup-s ⊢σ)) ⊢T
  presup-s-≈ (p-, ⊢τ ⊢T ⊢t)
    with ⊢Γ , ⊢Δpresup-s ⊢τ                 = ⊢Γ , ⊢p (⊢∷ ⊢Δ ⊢T) (s-, ⊢τ ⊢T ⊢t) , ⊢τ , ⊢Δ
  presup-s-≈ (,-ext ⊢σ)
    with ⊢Γ , ⊢TΔ@(⊢∷ ⊢Δ ⊢T)presup-s ⊢σ     = ⊢Γ , ⊢σ , s-, (⊢p ⊢TΔ ⊢σ) ⊢T (conv (t[σ] (vlookup ⊢TΔ here) ⊢σ) (≈-trans ([∘]-Se ⊢T (s-wk ⊢TΔ) ⊢σ) (≈-refl (t[σ]-Se ⊢T (⊢p ⊢TΔ ⊢σ))))) , ⊢TΔ
  presup-s-≈ (s-≈-sym σ≈τ)
    with ⊢Γ , ⊢σ , ⊢τ , ⊢Δpresup-s-≈ σ≈τ    = ⊢Γ , ⊢τ , ⊢σ , ⊢Δ
  presup-s-≈ (s-≈-trans σ≈σ′ σ′≈σ″)
    with ⊢Γ , ⊢σ , ⊢σ′ , _presup-s-≈ σ≈σ′
       | _  , _  , ⊢σ″ , ⊢Δpresup-s-≈ σ′≈σ″ = ⊢Γ , ⊢σ , ⊢σ″ , ⊢Δ
  presup-s-≈ (s-≈-conv σ≈τ Δ′≈Δ)
    with ⊢Γ , ⊢σ , ⊢τ , ⊢Δ′presup-s-≈ σ≈τ   = ⊢Γ , s-conv ⊢σ Δ′≈Δ , s-conv ⊢τ Δ′≈Δ , proj₂ (presup-⊢≈ Δ′≈Δ)