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

module NonCumulative.Statics.Ascribed.Simpl where

open import Lib

open import NonCumulative.Statics.Ascribed.Full
open import NonCumulative.Statics.Ascribed.Presup
open import NonCumulative.Statics.Ascribed.CtxEquiv


∷-cong-simp :  {i} 
               Γ  Δ 
              Γ  T  T′ ∶[ 1 + i ] Se i 
              ----------------
               (T  i)  Γ  (T′  i)  Δ
∷-cong-simp Γ≈Δ T≈T′
  with presup-≈ T≈T′
...  | _ , ⊢T , ⊢T′ , _ = ∷-cong Γ≈Δ ⊢T (ctxeq-tm Γ≈Δ ⊢T′) T≈T′ (ctxeq-≈ Γ≈Δ T≈T′)