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

-- Full formulation and Concise formulation are equivalent.
module Mints.Statics.Equiv where

open import Lib
open import Mints.Statics.Full as F
open import Mints.Statics.Concise as C
open import Mints.Statics.CtxEquiv
open import Mints.Statics.Presup
open import Mints.Statics.Misc
open import Mints.Statics.Properties.Box
open import Mints.Statics.Properties.Pi

mutual
  F⇒C-⊢ : F.⊢ Γ →
          -------
          C.⊢ Γ
  F⇒C-⊢ ⊢[]        = ⊢[]
  F⇒C-⊢ (⊢κ ⊢Γ)    = ⊢κ (F⇒C-⊢ ⊢Γ)
  F⇒C-⊢ (⊢∺ ⊢Γ ⊢T) = ⊢∺ (F⇒C-⊢ ⊢Γ) (F⇒C-tm ⊢T)


  F⇒C-tm : Γ F.⊢ t ∶ T →
           -------------
           Γ C.⊢ t ∶ T
  F⇒C-tm (N-wf i ⊢Γ)         = N-wf i (F⇒C-⊢ ⊢Γ)
  F⇒C-tm (Se-wf i ⊢Γ)        = Se-wf i (F⇒C-⊢ ⊢Γ)
  F⇒C-tm (Π-wf ⊢S ⊢T)        = Π-wf (F⇒C-tm ⊢S) (F⇒C-tm ⊢T)
  F⇒C-tm (□-wf ⊢T)           = □-wf (F⇒C-tm ⊢T)
  F⇒C-tm (vlookup ⊢Γ T∈Γ)    = vlookup (F⇒C-⊢ ⊢Γ) T∈Γ
  F⇒C-tm (ze-I ⊢Γ)           = ze-I (F⇒C-⊢ ⊢Γ)
  F⇒C-tm (su-I ⊢t)           = su-I (F⇒C-tm ⊢t)
  F⇒C-tm (N-E ⊢T ⊢s ⊢r ⊢t)   = N-E (F⇒C-tm ⊢T) (F⇒C-tm ⊢s) (F⇒C-tm ⊢r) (F⇒C-tm ⊢t)
  F⇒C-tm (Λ-I _ ⊢t)          = Λ-I (F⇒C-tm ⊢t)
  F⇒C-tm (Λ-E _ _ ⊢t ⊢r)     = Λ-E (F⇒C-tm ⊢t) (F⇒C-tm ⊢r)
  F⇒C-tm (□-I ⊢t)            = □-I (F⇒C-tm ⊢t)
  F⇒C-tm (□-E Ψs _ ⊢t ⊢Γ eq) = □-E Ψs (F⇒C-tm ⊢t) (F⇒C-⊢ ⊢Γ) eq
  F⇒C-tm (t[σ] ⊢t ⊢σ)        = t[σ] (F⇒C-tm ⊢t) (F⇒C-s ⊢σ)
  F⇒C-tm (cumu ⊢t)           = cumu (F⇒C-tm ⊢t)
  F⇒C-tm (conv ⊢t T≈T′)      = conv (F⇒C-tm ⊢t) (F⇒C-≈ T≈T′)


  F⇒C-s : Γ F.⊢s σ ∶ Δ →
          --------------
          Γ C.⊢s σ ∶ Δ
  F⇒C-s (s-I ⊢Γ)           = s-I (F⇒C-⊢ ⊢Γ)
  F⇒C-s (s-wk ⊢Γ)          = s-wk (F⇒C-⊢ ⊢Γ)
  F⇒C-s (s-∘ ⊢σ ⊢δ)        = s-∘ (F⇒C-s ⊢σ) (F⇒C-s ⊢δ)
  F⇒C-s (s-, ⊢σ ⊢T ⊢t)     = s-, (F⇒C-s ⊢σ) (F⇒C-tm ⊢T) (F⇒C-tm ⊢t)
  F⇒C-s (s-； Ψs ⊢σ ⊢Γ eq) = s-； Ψs (F⇒C-s ⊢σ) (F⇒C-⊢ ⊢Γ) eq
  F⇒C-s (s-conv ⊢σ Δ′≈Δ)   = s-conv (F⇒C-s ⊢σ) (F⇒C-⊢≈ Δ′≈Δ)


  F⇒C-⊢≈ : F.⊢ Γ ≈ Δ →
           -----------
           C.⊢ Γ ≈ Δ
  F⇒C-⊢≈ []-≈                    = []-≈
  F⇒C-⊢≈ (κ-cong Γ≈Δ)            = κ-cong (F⇒C-⊢≈ Γ≈Δ)
  F⇒C-⊢≈ (∺-cong Γ≈Δ _ _ T≈T′ _) = ∺-cong (F⇒C-⊢≈ Γ≈Δ) (F⇒C-≈ T≈T′)


  F⇒C-≈ : Γ F.⊢ t ≈ t′ ∶ T →
          ------------------
          Γ C.⊢ t ≈ t′ ∶ T
  F⇒C-≈ (N-[] i ⊢σ)                       = N-[] i (F⇒C-s ⊢σ)
  F⇒C-≈ (Se-[] i ⊢σ)                      = Se-[] i (F⇒C-s ⊢σ)
  F⇒C-≈ (Π-[] ⊢σ ⊢S ⊢T)                   = Π-[] (F⇒C-s ⊢σ) (F⇒C-tm ⊢S) (F⇒C-tm ⊢T)
  F⇒C-≈ (□-[] ⊢σ ⊢T)                      = □-[] (F⇒C-s ⊢σ) (F⇒C-tm ⊢T)
  F⇒C-≈ (Π-cong ⊢S S≈S′ T≈T′)             = Π-cong (F⇒C-≈ S≈S′) (F⇒C-≈ T≈T′)
  F⇒C-≈ (□-cong T≈T′)                     = □-cong (F⇒C-≈ T≈T′)
  F⇒C-≈ (v-≈ ⊢Γ T∈Γ)                      = v-≈ (F⇒C-⊢ ⊢Γ) T∈Γ
  F⇒C-≈ (ze-≈ ⊢Γ)                         = ze-≈ (F⇒C-⊢ ⊢Γ)
  F⇒C-≈ (su-cong t≈t′)                    = su-cong (F⇒C-≈ t≈t′)
  F⇒C-≈ (rec-cong ⊢T T≈T′ s≈s′ r≈r′ t≈t′) = rec-cong (F⇒C-≈ T≈T′) (F⇒C-≈ s≈s′) (F⇒C-≈ r≈r′) (F⇒C-≈ t≈t′)
  F⇒C-≈ (Λ-cong ⊢S t≈t′)                  = Λ-cong (F⇒C-≈ t≈t′)
  F⇒C-≈ ($-cong _ _ t≈t′ r≈r′)            = $-cong (F⇒C-≈ t≈t′) (F⇒C-≈ r≈r′)
  F⇒C-≈ (box-cong t≈t′)                   = box-cong (F⇒C-≈ t≈t′)
  F⇒C-≈ (unbox-cong Ψs _ t≈t′ ⊢Γ eq)      = unbox-cong Ψs (F⇒C-≈ t≈t′) (F⇒C-⊢ ⊢Γ) eq
  F⇒C-≈ ([]-cong t≈t′ σ≈σ′)               = []-cong (F⇒C-≈ t≈t′) (F⇒C-s-≈ σ≈σ′)
  F⇒C-≈ (ze-[] ⊢σ)                        = ze-[] (F⇒C-s ⊢σ)
  F⇒C-≈ (su-[] ⊢σ ⊢t)                     = su-[] (F⇒C-s ⊢σ) (F⇒C-tm ⊢t)
  F⇒C-≈ (rec-[] ⊢σ ⊢T ⊢s ⊢r ⊢t)           = rec-[] (F⇒C-s ⊢σ) (F⇒C-tm ⊢T) (F⇒C-tm ⊢s) (F⇒C-tm ⊢r) (F⇒C-tm ⊢t)
  F⇒C-≈ (Λ-[] ⊢σ ⊢t)                      = Λ-[] (F⇒C-s ⊢σ) (F⇒C-tm ⊢t)
  F⇒C-≈ ($-[] _ _ ⊢σ ⊢t ⊢s)               = $-[] (F⇒C-s ⊢σ) (F⇒C-tm ⊢t) (F⇒C-tm ⊢s)
  F⇒C-≈ (box-[] ⊢σ ⊢t)                    = box-[] (F⇒C-s ⊢σ) (F⇒C-tm ⊢t)
  F⇒C-≈ (unbox-[] Ψs _ ⊢t ⊢σ eq)          = unbox-[] Ψs (F⇒C-tm ⊢t) (F⇒C-s ⊢σ) eq
  F⇒C-≈ (rec-β-ze ⊢T ⊢s ⊢r)               = rec-β-ze (F⇒C-tm ⊢T) (F⇒C-tm ⊢s) (F⇒C-tm ⊢r)
  F⇒C-≈ (rec-β-su ⊢T ⊢s ⊢r ⊢t)            = rec-β-su (F⇒C-tm ⊢T) (F⇒C-tm ⊢s) (F⇒C-tm ⊢r) (F⇒C-tm ⊢t)
  F⇒C-≈ (Λ-β _ _ ⊢t ⊢s)                   = Λ-β (F⇒C-tm ⊢t) (F⇒C-tm ⊢s)
  F⇒C-≈ (Λ-η _ _ ⊢t)                      = Λ-η (F⇒C-tm ⊢t)
  F⇒C-≈ (□-β Ψs _ ⊢t ⊢Γ eq)               = □-β Ψs (F⇒C-tm ⊢t) (F⇒C-⊢ ⊢Γ) eq
  F⇒C-≈ (□-η _ ⊢t)                        = □-η (F⇒C-tm ⊢t)
  F⇒C-≈ ([I] ⊢t)                          = [I] (F⇒C-tm ⊢t)
  F⇒C-≈ ([wk] ⊢SΓ T∈Γ)                    = [wk] (F⇒C-⊢ ⊢SΓ) T∈Γ
  F⇒C-≈ ([∘] ⊢δ ⊢σ ⊢t)                    = [∘] (F⇒C-s ⊢δ) (F⇒C-s ⊢σ) (F⇒C-tm ⊢t)
  F⇒C-≈ ([,]-v-ze ⊢σ ⊢S ⊢t)               = [,]-v-ze (F⇒C-s ⊢σ) (F⇒C-tm ⊢S) (F⇒C-tm ⊢t)
  F⇒C-≈ ([,]-v-su ⊢σ ⊢S ⊢t T∈Δ)           = [,]-v-su (F⇒C-s ⊢σ) (F⇒C-tm ⊢S) (F⇒C-tm ⊢t) T∈Δ
  F⇒C-≈ (≈-cumu t≈t′)                     = ≈-cumu (F⇒C-≈ t≈t′)
  F⇒C-≈ (≈-conv t≈t′ S≈T)                 = ≈-conv (F⇒C-≈ t≈t′) (F⇒C-≈ S≈T)
  F⇒C-≈ (≈-sym t≈t′)                      = ≈-sym (F⇒C-≈ t≈t′)
  F⇒C-≈ (≈-trans t≈t′ t′≈t″)              = ≈-trans (F⇒C-≈ t≈t′) (F⇒C-≈ t′≈t″)


  F⇒C-s-≈ : Γ F.⊢s σ ≈ σ′ ∶ Δ →
            ------------------
            Γ C.⊢s σ ≈ σ′ ∶ Δ
  F⇒C-s-≈ (I-≈ ⊢Γ)                = I-≈ (F⇒C-⊢ ⊢Γ)
  F⇒C-s-≈ (wk-≈ ⊢TΓ)              = wk-≈ (F⇒C-⊢ ⊢TΓ)
  F⇒C-s-≈ (∘-cong σ≈σ′ δ≈δ′)      = ∘-cong (F⇒C-s-≈ σ≈σ′) (F⇒C-s-≈ δ≈δ′)
  F⇒C-s-≈ (,-cong σ≈σ′ ⊢T t≈t′)   = ,-cong (F⇒C-s-≈ σ≈σ′) (F⇒C-tm ⊢T) (F⇒C-≈ t≈t′)
  F⇒C-s-≈ (；-cong Ψs σ≈σ′ ⊢Γ eq) = ；-cong Ψs (F⇒C-s-≈ σ≈σ′) (F⇒C-⊢ ⊢Γ) eq
  F⇒C-s-≈ (I-∘ ⊢σ)                = I-∘ (F⇒C-s ⊢σ)
  F⇒C-s-≈ (∘-I ⊢σ)                = ∘-I (F⇒C-s ⊢σ)
  F⇒C-s-≈ (∘-assoc ⊢σ ⊢σ′ ⊢σ″)    = ∘-assoc (F⇒C-s ⊢σ) (F⇒C-s ⊢σ′) (F⇒C-s ⊢σ″)
  F⇒C-s-≈ (,-∘ ⊢σ ⊢T ⊢t ⊢δ)       = ,-∘ (F⇒C-s ⊢σ) (F⇒C-tm ⊢T) (F⇒C-tm ⊢t) (F⇒C-s ⊢δ)
  F⇒C-s-≈ (；-∘ Ψs ⊢σ ⊢δ ⊢Γ eq)   = ；-∘ Ψs (F⇒C-s ⊢σ) (F⇒C-s ⊢δ) eq
  F⇒C-s-≈ (p-, ⊢σ ⊢T ⊢t)          = p-, (F⇒C-s ⊢σ) (F⇒C-tm ⊢T) (F⇒C-tm ⊢t)
  F⇒C-s-≈ (,-ext ⊢σ)              = ,-ext (F⇒C-s ⊢σ)
  F⇒C-s-≈ (；-ext ⊢σ)             = ；-ext (F⇒C-s ⊢σ)
  F⇒C-s-≈ (s-≈-sym σ≈σ′)          = s-≈-sym (F⇒C-s-≈ σ≈σ′)
  F⇒C-s-≈ (s-≈-trans σ≈σ′ σ′≈σ″)  = s-≈-trans (F⇒C-s-≈ σ≈σ′) (F⇒C-s-≈ σ′≈σ″)
  F⇒C-s-≈ (s-≈-conv σ≈σ′ Δ′≈Δ)    = s-≈-conv (F⇒C-s-≈ σ≈σ′) (F⇒C-⊢≈ Δ′≈Δ)


mutual
  C⇒F-⊢ : C.⊢ Γ →
          -------
          F.⊢ Γ
  C⇒F-⊢ ⊢[]        = ⊢[]
  C⇒F-⊢ (⊢κ ⊢Γ)    = ⊢κ (C⇒F-⊢ ⊢Γ)
  C⇒F-⊢ (⊢∺ ⊢Γ ⊢T) = ⊢∺ (C⇒F-⊢ ⊢Γ) (C⇒F-tm ⊢T)


  C⇒F-tm : Γ C.⊢ t ∶ T →
           -------------
           Γ F.⊢ t ∶ T
  C⇒F-tm (N-wf i ⊢Γ)                              = N-wf i (C⇒F-⊢ ⊢Γ)
  C⇒F-tm (Se-wf i ⊢Γ)                             = Se-wf i (C⇒F-⊢ ⊢Γ)
  C⇒F-tm (Π-wf ⊢S ⊢T)                             = Π-wf (C⇒F-tm ⊢S) (C⇒F-tm ⊢T)
  C⇒F-tm (□-wf ⊢T)                                = □-wf (C⇒F-tm ⊢T)
  C⇒F-tm (vlookup ⊢Γ T∈Γ)                         = vlookup (C⇒F-⊢ ⊢Γ) T∈Γ
  C⇒F-tm (ze-I ⊢Γ)                                = ze-I (C⇒F-⊢ ⊢Γ)
  C⇒F-tm (su-I ⊢t)                                = su-I (C⇒F-tm ⊢t)
  C⇒F-tm (N-E ⊢T ⊢s ⊢r ⊢t)                        = N-E (C⇒F-tm ⊢T) (C⇒F-tm ⊢s) (C⇒F-tm ⊢r) (C⇒F-tm ⊢t)
  C⇒F-tm (Λ-I ⊢t)
    with ⊢∺ ⊢Γ ⊢S ← proj₁ (presup-tm (C⇒F-tm ⊢t)) = Λ-I ⊢S (C⇒F-tm ⊢t)
  C⇒F-tm (Λ-E ⊢t ⊢r)
    with _ , _ , ⊢Π ← presup-tm (C⇒F-tm ⊢t)       = Λ-E (lift-⊢-Se-max (proj₂ (inv-Π-wf′ ⊢Π))) (lift-⊢-Se-max′ (proj₂ (inv-Π-wf ⊢Π))) (C⇒F-tm ⊢t) (C⇒F-tm ⊢r)
  C⇒F-tm (□-I ⊢t)                                 = □-I (C⇒F-tm ⊢t)
  C⇒F-tm (□-E Ψs ⊢t ⊢Γ eq)
    with _ , _ , ⊢□ ← presup-tm (C⇒F-tm ⊢t)       = □-E Ψs (proj₂ (inv-□-wf ⊢□)) (C⇒F-tm ⊢t) (C⇒F-⊢ ⊢Γ) eq
  C⇒F-tm (t[σ] ⊢t ⊢σ)                             = t[σ] (C⇒F-tm ⊢t) (C⇒F-s ⊢σ)
  C⇒F-tm (cumu ⊢t)                                = cumu (C⇒F-tm ⊢t)
  C⇒F-tm (conv ⊢t T≈T′)                           = conv (C⇒F-tm ⊢t) (C⇒F-≈ T≈T′)


  C⇒F-s : Γ C.⊢s σ ∶ Δ →
          --------------
          Γ F.⊢s σ ∶ Δ
  C⇒F-s (s-I ⊢Γ)           = s-I (C⇒F-⊢ ⊢Γ)
  C⇒F-s (s-wk ⊢TΓ)         = s-wk (C⇒F-⊢ ⊢TΓ)
  C⇒F-s (s-∘ ⊢σ ⊢δ)        = s-∘ (C⇒F-s ⊢σ) (C⇒F-s ⊢δ)
  C⇒F-s (s-, ⊢σ ⊢T ⊢t)     = s-, (C⇒F-s ⊢σ) (C⇒F-tm ⊢T) (C⇒F-tm ⊢t)
  C⇒F-s (s-； Ψs ⊢σ ⊢Γ eq) = s-； Ψs (C⇒F-s ⊢σ) (C⇒F-⊢ ⊢Γ) eq
  C⇒F-s (s-conv ⊢σ Δ′≈Δ)   = s-conv (C⇒F-s ⊢σ) (C⇒F-⊢≈ Δ′≈Δ)


  C⇒F-⊢≈ : C.⊢ Γ ≈ Δ →
           -----------
           F.⊢ Γ ≈ Δ
  C⇒F-⊢≈ []-≈                                        = []-≈
  C⇒F-⊢≈ (κ-cong Γ≈Δ)                                = κ-cong (C⇒F-⊢≈ Γ≈Δ)
  C⇒F-⊢≈ (∺-cong Γ≈Δ T≈T′)
    with T≈T′₁ ← ctxeq-≈ (C⇒F-⊢≈ Γ≈Δ) (C⇒F-≈ T≈T′)
       with _ , ⊢T , _       ← presup-≈ (C⇒F-≈ T≈T′)
          | _ , _  , ⊢T′ , _ ← presup-≈ T≈T′₁        = ∺-cong (C⇒F-⊢≈ Γ≈Δ) ⊢T ⊢T′ (C⇒F-≈ T≈T′) T≈T′₁


  C⇒F-≈ : Γ C.⊢ t ≈ t′ ∶ T →
          ------------------
          Γ F.⊢ t ≈ t′ ∶ T
  C⇒F-≈ (N-[] i ⊢σ)                                 = N-[] i (C⇒F-s ⊢σ)
  C⇒F-≈ (Se-[] i ⊢σ)                                = Se-[] i (C⇒F-s ⊢σ)
  C⇒F-≈ (Π-[] ⊢σ ⊢S ⊢T)                             = Π-[] (C⇒F-s ⊢σ) (C⇒F-tm ⊢S) (C⇒F-tm ⊢T)
  C⇒F-≈ (□-[] ⊢σ ⊢T)                                = □-[] (C⇒F-s ⊢σ) (C⇒F-tm ⊢T)
  C⇒F-≈ (Π-cong S≈S′ T≈T′)
    with _ , ⊢S , _ ← presup-≈ (C⇒F-≈ S≈S′)         = Π-cong ⊢S (C⇒F-≈ S≈S′) (C⇒F-≈ T≈T′)
  C⇒F-≈ (□-cong T≈T′)                               = □-cong (C⇒F-≈ T≈T′)
  C⇒F-≈ (v-≈ ⊢Γ T∈Γ)                                = v-≈ (C⇒F-⊢ ⊢Γ) T∈Γ
  C⇒F-≈ (ze-≈ ⊢Γ)                                   = ze-≈ (C⇒F-⊢ ⊢Γ)
  C⇒F-≈ (su-cong t≈t′)                              = su-cong (C⇒F-≈ t≈t′)
  C⇒F-≈ (rec-cong T≈T′ s≈s′ r≈r′ t≈t′)
    with _ , ⊢T , _ ← presup-≈ (C⇒F-≈ T≈T′)         = rec-cong ⊢T (C⇒F-≈ T≈T′) (C⇒F-≈ s≈s′) (C⇒F-≈ r≈r′) (C⇒F-≈ t≈t′)
  C⇒F-≈ (Λ-cong t≈t′)
    with ⊢∺ ⊢Γ ⊢S , _ ← presup-≈ (C⇒F-≈ t≈t′)       = Λ-cong ⊢S (C⇒F-≈ t≈t′)
  C⇒F-≈ ($-cong t≈t′ r≈r′)
    with _ , _ , _ , _ , ⊢Π ← presup-≈ (C⇒F-≈ t≈t′) = $-cong (lift-⊢-Se-max (proj₂ (inv-Π-wf′ ⊢Π))) (lift-⊢-Se-max′ (proj₂ (inv-Π-wf ⊢Π))) (C⇒F-≈ t≈t′) (C⇒F-≈ r≈r′)
  C⇒F-≈ (box-cong t≈t′)                             = box-cong (C⇒F-≈ t≈t′)
  C⇒F-≈ (unbox-cong Ψs t≈t′ ⊢Γ eq)
    with _ , _ , _ , _ , ⊢□ ← presup-≈ (C⇒F-≈ t≈t′) = unbox-cong Ψs (proj₂ (inv-□-wf ⊢□)) (C⇒F-≈ t≈t′) (C⇒F-⊢ ⊢Γ) eq
  C⇒F-≈ ([]-cong t≈t′ σ≈σ′)                         = []-cong (C⇒F-≈ t≈t′) (C⇒F-s-≈ σ≈σ′)
  C⇒F-≈ (ze-[] ⊢σ)                                  = ze-[] (C⇒F-s ⊢σ)
  C⇒F-≈ (su-[] ⊢σ ⊢t)                               = su-[] (C⇒F-s ⊢σ) (C⇒F-tm ⊢t)
  C⇒F-≈ (rec-[] ⊢σ ⊢T ⊢s ⊢r ⊢t)                     = rec-[] (C⇒F-s ⊢σ) (C⇒F-tm ⊢T) (C⇒F-tm ⊢s) (C⇒F-tm ⊢r) (C⇒F-tm ⊢t)
  C⇒F-≈ (Λ-[] ⊢σ ⊢t)                                = Λ-[] (C⇒F-s ⊢σ) (C⇒F-tm ⊢t)
  C⇒F-≈ ($-[] ⊢σ ⊢t ⊢s)
    with _ , _ , ⊢Π ← presup-tm (C⇒F-tm ⊢t)         = $-[] (lift-⊢-Se-max (proj₂ (inv-Π-wf′ ⊢Π))) (lift-⊢-Se-max′ (proj₂ (inv-Π-wf ⊢Π))) (C⇒F-s ⊢σ) (C⇒F-tm ⊢t) (C⇒F-tm ⊢s)
  C⇒F-≈ (box-[] ⊢σ ⊢t)                              = box-[] (C⇒F-s ⊢σ) (C⇒F-tm ⊢t)
  C⇒F-≈ (unbox-[] Ψs ⊢t ⊢σ eq)
    with _ , _ , ⊢□ ← presup-tm (C⇒F-tm ⊢t)         = unbox-[] Ψs (proj₂ (inv-□-wf ⊢□)) (C⇒F-tm ⊢t) (C⇒F-s ⊢σ) eq
  C⇒F-≈ (rec-β-ze ⊢T ⊢s ⊢r)                         = rec-β-ze (C⇒F-tm ⊢T) (C⇒F-tm ⊢s) (C⇒F-tm ⊢r)
  C⇒F-≈ (rec-β-su ⊢T ⊢s ⊢r ⊢t)                      = rec-β-su (C⇒F-tm ⊢T) (C⇒F-tm ⊢s) (C⇒F-tm ⊢r) (C⇒F-tm ⊢t)
  C⇒F-≈ (Λ-β ⊢t ⊢s)
    with ⊢∺ ⊢Γ ⊢S , _ , ⊢T ← presup-tm (C⇒F-tm ⊢t)  = Λ-β (lift-⊢-Se-max ⊢S) (lift-⊢-Se-max′ ⊢T) (C⇒F-tm ⊢t) (C⇒F-tm ⊢s)
  C⇒F-≈ (Λ-η ⊢t)
    with _ , _ , ⊢Π ← presup-tm (C⇒F-tm ⊢t)         = Λ-η (lift-⊢-Se-max (proj₂ (inv-Π-wf′ ⊢Π))) (lift-⊢-Se-max′ (proj₂ (inv-Π-wf ⊢Π))) (C⇒F-tm ⊢t)
  C⇒F-≈ (□-β Ψs ⊢t ⊢Γ eq)
    with _ , _ , ⊢T ← presup-tm (C⇒F-tm ⊢t)         = □-β Ψs ⊢T (C⇒F-tm ⊢t) (C⇒F-⊢ ⊢Γ) eq
  C⇒F-≈ (□-η ⊢t)
    with _ , _ , ⊢□ ← presup-tm (C⇒F-tm ⊢t)         = □-η (proj₂ (inv-□-wf ⊢□)) (C⇒F-tm ⊢t)
  C⇒F-≈ ([I] ⊢t)                                    = [I] (C⇒F-tm ⊢t)
  C⇒F-≈ ([wk] ⊢SΓ T∈Γ)                              = [wk] (C⇒F-⊢ ⊢SΓ) T∈Γ
  C⇒F-≈ ([∘] ⊢δ ⊢σ ⊢t)                              = [∘] (C⇒F-s ⊢δ) (C⇒F-s ⊢σ) (C⇒F-tm ⊢t)
  C⇒F-≈ ([,]-v-ze ⊢σ ⊢S ⊢t)                         = [,]-v-ze (C⇒F-s ⊢σ) (C⇒F-tm ⊢S) (C⇒F-tm ⊢t)
  C⇒F-≈ ([,]-v-su ⊢σ ⊢S ⊢t T∈Δ)                     = [,]-v-su (C⇒F-s ⊢σ) (C⇒F-tm ⊢S) (C⇒F-tm ⊢t) T∈Δ
  C⇒F-≈ (≈-cumu t≈t′)                               = ≈-cumu (C⇒F-≈ t≈t′)
  C⇒F-≈ (≈-conv t≈t′ S≈T)                           = ≈-conv (C⇒F-≈ t≈t′) (C⇒F-≈ S≈T)
  C⇒F-≈ (≈-sym t≈t′)                                = ≈-sym (C⇒F-≈ t≈t′)
  C⇒F-≈ (≈-trans t≈t′ t′≈t″)                        = ≈-trans (C⇒F-≈ t≈t′) (C⇒F-≈ t′≈t″)


  C⇒F-s-≈ : Γ C.⊢s σ ≈ σ′ ∶ Δ →
            ------------------
            Γ F.⊢s σ ≈ σ′ ∶ Δ
  C⇒F-s-≈ (I-≈ ⊢Γ)                = I-≈ (C⇒F-⊢ ⊢Γ)
  C⇒F-s-≈ (wk-≈ ⊢TΓ)              = wk-≈ (C⇒F-⊢ ⊢TΓ)
  C⇒F-s-≈ (∘-cong σ≈σ′ δ≈δ′)      = ∘-cong (C⇒F-s-≈ σ≈σ′) (C⇒F-s-≈ δ≈δ′)
  C⇒F-s-≈ (,-cong σ≈σ′ ⊢T t≈t′)   = ,-cong (C⇒F-s-≈ σ≈σ′) (C⇒F-tm ⊢T) (C⇒F-≈ t≈t′)
  C⇒F-s-≈ (；-cong Ψs σ≈σ′ ⊢Γ eq) = ；-cong Ψs (C⇒F-s-≈ σ≈σ′) (C⇒F-⊢ ⊢Γ) eq
  C⇒F-s-≈ (I-∘ ⊢σ)                = I-∘ (C⇒F-s ⊢σ)
  C⇒F-s-≈ (∘-I ⊢σ)                = ∘-I (C⇒F-s ⊢σ)
  C⇒F-s-≈ (∘-assoc ⊢σ ⊢σ′ ⊢σ″)    = ∘-assoc (C⇒F-s ⊢σ) (C⇒F-s ⊢σ′) (C⇒F-s ⊢σ″)
  C⇒F-s-≈ (,-∘ ⊢σ ⊢T ⊢t ⊢δ)       = ,-∘ (C⇒F-s ⊢σ) (C⇒F-tm ⊢T) (C⇒F-tm ⊢t) (C⇒F-s ⊢δ)
  C⇒F-s-≈ (；-∘ Ψs ⊢σ ⊢δ eq)      = ；-∘ Ψs (C⇒F-s ⊢σ) (C⇒F-s ⊢δ) (proj₂ (presup-s (C⇒F-s ⊢δ))) eq
  C⇒F-s-≈ (p-, ⊢σ ⊢T ⊢t)          = p-, (C⇒F-s ⊢σ) (C⇒F-tm ⊢T) (C⇒F-tm ⊢t)
  C⇒F-s-≈ (,-ext ⊢σ)              = ,-ext (C⇒F-s ⊢σ)
  C⇒F-s-≈ (；-ext ⊢σ)             = ；-ext (C⇒F-s ⊢σ)
  C⇒F-s-≈ (s-≈-sym σ≈σ′)          = s-≈-sym (C⇒F-s-≈ σ≈σ′)
  C⇒F-s-≈ (s-≈-trans σ≈σ′ σ′≈σ″)  = s-≈-trans (C⇒F-s-≈ σ≈σ′) (C⇒F-s-≈ σ′≈σ″)
  C⇒F-s-≈ (s-≈-conv σ≈σ′ Δ′≈Δ)    = s-≈-conv (C⇒F-s-≈ σ≈σ′) (C⇒F-⊢≈ Δ′≈Δ)