{-# OPTIONS --safe #-}
{-# OPTIONS --with-K #-}

-- Decidable equality for terms, substitutions, and patterns

module Pat.Term.Equality where

open import Data.Maybe using (Maybe; just; nothing; _>>=_)
open import Relation.Nullary.Decidable.Core using (Dec; yes; no; dec⇒maybe)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; ≡-≟-identity) renaming (subst to transport)
open import Relation.Nullary using (¬_)
open import Axiom.UniquenessOfIdentityProofs.WithK using (uip)

open import Pat.Context
open import Pat.Context.Equality
open import Pat.Term

-- We define decidable equality following G. Allais's approach, which requires only a linear number of cases.
-- The key idea is to implement a `view` function that takes two inputs and returns `Maybe (x ≡ y)`.
-- Then, we prove its completeness through a lemma: `view-diag : view x x ≡ just refl`.
-- With the `view` function and the `view-diag` lemma, we can derive decidable equality for the type.
-- Reference: https://github.com/gallais/potpourri/blob/main/agda/poc/LinearDec.agda

-- `view` functions for terms, substitutions, and patterns.
-- These definitions may seem complex, but their correctness
-- is ensured their types and the `view-diag` lemmas.
viewᵉ : (e₁ e₂ : Term n Γ A) → Maybe (e₁ ≡ e₂)
viewᵖ : (p₁ p₂ : Pattern n Γ Δ A Π) → Maybe (p₁ ≡ p₂)
viewˢ : (σ₁ σ₂ : Subst Γ Γ′) → Maybe (σ₁ ≡ σ₂)
viewˢᵖ : (π₁ π₂ : Γ ∣ Δ ⊩ Δ′ ↝ Π) → Maybe (π₁ ≡ π₂)

viewᵉ (`_`with_ {Δ = Δ₁} x₁ σ₁)  (`_`with_ {Δ = Δ₂} x₂ σ₂) = do
  refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
  refl ← dec⇒maybe (x₁ ≟ˣ x₂)
  refl ← viewˢ σ₁ σ₂
  just refl
viewᵉ `true `true = just refl
viewᵉ `false `false = just refl
viewᵉ (`if e₁ `then e₂ `else e₃) (`if e₁′ `then e₂′ `else e₃′) = do
  refl ← viewᵉ e₁ e₁′
  refl ← viewᵉ e₂ e₂′
  refl ← viewᵉ e₃ e₃′
  just refl
viewᵉ (`λ⟨ Δ₁ ⟩ e₁) (`λ⟨ Δ₂ ⟩ e₂) = do
  refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
  refl ← viewᵉ e₁ e₂
  just refl
viewᵉ (_·_ {Δ = Δ₁} {A = A₁} e₁ e₂) (_·_ {Δ = Δ₂} {A = A₂} e₁′ e₂′) = do
  refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
  refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
  refl ← viewᵉ e₁ e₁′
  refl ← viewᵉ e₂ e₂′
  just refl
viewᵉ ⟨ e₁ ⟩ ⟨ e₂ ⟩ = do
  refl ← viewᵉ e₁ e₂
  just refl
viewᵉ (`let⟨_⟩ {A = A₁} Δ₁ e₁ e₂) (`let⟨_⟩ {A = A₂} Δ₂ e₁′ e₂′) = do
  refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
  refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
  refl ← viewᵉ e₁ e₁′
  refl ← viewᵉ e₂ e₂′
  just refl
viewᵉ (`wrap Δ₁ e₁) (`wrap Δ₂ e₂) = do
  refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
  refl ← viewᵉ e₁ e₂
  just refl
viewᵉ (`letwrap {A = A₁} Δ₁ e₁ e₂) (`letwrap {A = A₂} Δ₂ e₁′ e₂′) = do
  refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
  refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
  refl ← viewᵉ e₁ e₁′
  refl ← viewᵉ e₂ e₂′
  just refl
viewᵉ (`iflet⟨_⟩ {A = A₁} {Π = Π₁} Δ₁ p e₁ e₂ e₃) (`iflet⟨_⟩ {A = A₂} {Π = Π₂} Δ₂ p' e₁′ e₂′ e₃′) = do
  refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
  refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
  refl ← dec⇒maybe (Π₁ ≟ᶜ Π₂)
  refl ← viewᵖ p p'
  refl ← viewᵉ e₁ e₁′
  refl ← viewᵉ e₂ e₂′
  refl ← viewᵉ e₃ e₃′
  just refl
viewᵉ (`rewritȩ {A = A₁} {Π = Π₁} p e₁ e₂) (`rewritȩ {A = A₂} {Π = Π₂} p′ e₁′ e₂′) = do
  refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
  refl ← dec⇒maybe (Π₁ ≟ᶜ Π₂)
  refl ← viewᵖ p p′
  refl ← viewᵉ e₁ e₁′
  refl ← viewᵉ e₂ e₂′
  just refl
viewᵉ _ _ = nothing


viewᵖ p₁ p₂ = viewᵖ' refl p₁ p₂ where
  viewᵖ' : (eq : Π ≡ Π′) (p₁ : Pattern n Γ Δ A Π) (p₂ : Pattern n Γ Δ A Π′) → Maybe (transport (Pattern n Γ Δ A) eq p₁ ≡ p₂)
  viewᵖ' eq `pat `pat with refl ← eq = just refl
  viewᵖ' eq (`_`with₁_ {Δ′ = Δ₁} x₁ σ₁) (`_`with₁_ {Δ′ = Δ₂} x₂ σ₂) with refl ← eq = do
    refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
    refl ← dec⇒maybe (x₁ ≟ˣ x₂)
    refl ← viewˢ σ₁ σ₂
    just refl
  viewᵖ' eq (`_`with₂_ {Δ′ = Δ₁} x₁ π₁) (`_`with₂_ {Δ′ = Δ₂} x₂ π₂) with refl ← eq = do
    refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
    refl ← dec⇒maybe (x₁ ≟ˣ x₂)
    refl ← viewˢᵖ π₁ π₂
    just refl
  viewᵖ' eq `true `true with refl ← eq = just refl
  viewᵖ' eq `false `false with refl ← eq = just refl
  viewᵖ' eq p@(`if_`then_`else_ {Π₁ = Π₁} {Π₂ = Π₂} {Π₃ = Π₃} p₁ p₂ p₃) (`if_`then_`else_ {Π₁ = Π₁′} {Π₂ = Π₂′} {Π₃ = Π₃′} p₁′ p₂′ p₃′) = do
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← dec⇒maybe (Π₃ ≟ᶜ Π₃′)
    refl ← viewᵖ p₁ p₁′
    refl ← viewᵖ p₂ p₂′
    refl ← viewᵖ p₃ p₃′
    refl ← just (uip eq refl)
    just refl
  viewᵖ' eq (`λ⟨ Δ₁ ⟩ p₁) (`λ⟨ Δ₂ ⟩ p₂) with refl ← eq = do
    refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
    refl ← viewᵖ p₁ p₂
    just refl
  viewᵖ' eq (_·_ {Δ′ = Δ₁} {A = A₁} {Π₁ = Π₁} {Π₂ = Π₂} p₁ p₂) (_·_ {Δ′ = Δ₂} {A = A₂} {Π₁ = Π₁′} {Π₂ = Π₂′} p₁′ p₂′) = do
    refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
    refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← viewᵖ p₁ p₁′
    refl ← viewᵖ p₂ p₂′
    refl ← just (uip eq refl)
    just refl
  viewᵖ' eq (⟨_⟩ {Π = Π₁} p₁) (⟨_⟩ {Π = Π₂} p₂) = do
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₂)
    refl ← viewᵖ p₁ p₂
    refl ← just (uip eq refl)
    just refl
  viewᵖ' eq (`let⟨_⟩ {A = A₁} {Π₁ = Π₁} {Π₂ = Π₂} Δ₁ p₁ p₂) (`let⟨_⟩ {A = A₂} {Π₁ = Π₁′} {Π₂ = Π₂′} Δ₂ p₁′ p₂′) = do
    refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
    refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← viewᵖ p₁ p₁′
    refl ← viewᵖ p₂ p₂′
    refl ← just (uip eq refl)
    just refl
  viewᵖ' eq (`wrap Δ₁ p₁) (`wrap Δ₂ p₂) with refl ← eq = do
    refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
    refl ← viewᵖ p₁ p₂
    just refl
  viewᵖ' eq (`letwrap {A = A₁} {Π₁ = Π₁} {Π₂ = Π₂} Δ′₁ p₁ p₂) (`letwrap {A = A₂} {Π₁ = Π₁′} {Π₂ = Π₂′} Δ′₂ p₁′ p₂′) = do
    refl ← dec⇒maybe (Δ′₁ ≟ᶜ Δ′₂)
    refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← viewᵖ p₁ p₁′
    refl ← viewᵖ p₂ p₂′
    refl ← just (uip eq refl)
    just refl
  viewᵖ' eq (`iflet⟨_⟩ {A = A₁} {Π = Π} {Π₁ = Π₁} {Π₂ = Π₂} {Π₃ = Π₃} Δ₁ p e₁ e₂ e₃)
            (`iflet⟨_⟩ {A = A₂} {Π = Π′} {Π₁ = Π₁′} {Π₂ = Π₂′} {Π₃ = Π₃′} Δ₂ p' e₁' e₂' e₃') = do
    refl ← dec⇒maybe (Δ₁ ≟ᶜ Δ₂)
    refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
    refl ← dec⇒maybe (Π ≟ᶜ Π′)
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← dec⇒maybe (Π₃ ≟ᶜ Π₃′)
    refl ← viewᵖ p p'
    refl ← viewᵖ e₁ e₁'
    refl ← viewᵖ e₂ e₂'
    refl ← viewᵖ e₃ e₃'
    refl ← just (uip eq refl)
    just refl
  viewᵖ' eq (`rewritȩ {A = A₁} {Π = Π} {Π₁ = Π₁} {Π₂ = Π₂} p p₁ p₂) (`rewritȩ {A = A₂} {Π = Π′} {Π₁ = Π₁′} {Π₂ = Π₂′} p′ p₁′ p₂′) = do
    refl ← dec⇒maybe (A₁ ≟ᵗ A₂)
    refl ← dec⇒maybe (Π ≟ᶜ Π′)
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← viewᵖ p p′
    refl ← viewᵖ p₁ p₁′
    refl ← viewᵖ p₂ p₂′
    refl ← just (uip eq refl)
    just refl
  viewᵖ' _ _ _ = nothing


viewˢ ∅ ∅ = just refl
viewˢ (σ₁ , term e₁) (σ₂ , term e₂) = do
  refl ← viewᵉ e₁ e₂
  refl ← viewˢ σ₁ σ₂
  just refl
viewˢ (σ₁ , var x₁) (σ₂ , var x₂) = do
  refl ← dec⇒maybe (x₁ ≟ˣ x₂)
  refl ← viewˢ σ₁ σ₂
  just refl
viewˢ _ _ = nothing


viewˢᵖ = viewˢᵖ' refl where
  viewˢᵖ' : (eq : Π ≡ Π′) (π₁ : Γ ∣ Δ ⊩ Δ′ ↝ Π) (π₂ : Γ ∣ Δ ⊩ Δ′ ↝ Π′) → Maybe (transport (Γ ∣ Δ ⊩ Δ′ ↝_) eq π₁ ≡ π₂)

  viewˢᵖ' eq ∅ ∅ with refl ← eq = just refl
  viewˢᵖ' eq (_,_ {Π₁ = Π₁} {Π₂ = Π₂} π (term p)) (_,_ {Π₁ = Π₁′} {Π₂ = Π₂′} π′ (term p′)) = do
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← viewᵖ p p′
    refl ← viewˢᵖ π π′
    refl ← just (uip eq refl)
    just refl
  viewˢᵖ' eq (_,_ {Π₁ = Π₁} {Π₂ = Π₂} π (var x)) (_,_ {Π₁ = Π₁′} {Π₂ = Π₂′} π′ (var x′)) = do
    refl ← dec⇒maybe (Π₁ ≟ᶜ Π₁′)
    refl ← dec⇒maybe (Π₂ ≟ᶜ Π₂′)
    refl ← dec⇒maybe (x ≟ˣ x′)
    refl ← viewˢᵖ π π′
    refl ← just (uip eq refl)
    just refl
  viewˢᵖ' _ _ _ = nothing


≟-diag : ∀ {ℓ} {A : Set ℓ} → (_≟_ : DecidableEquality A) → (x : A) → _≟_ x x ≡ yes refl
≟-diag _≟_ x = ≡-≟-identity _≟_ {x = x} refl

-- The `view-diag` lemmas
viewᵉ-diag : (e : Term n Γ A) → viewᵉ e e ≡ just refl
viewᵖ-diag : (p : Pattern n Γ Δ A Π) → viewᵖ p p ≡ just refl
viewˢ-diag : (σ : Subst Γ Γ′) → viewˢ σ σ ≡ just refl
viewˢᵖ-diag : (π : Γ ∣ Δ ⊩ Δ′ ↝ Π) → viewˢᵖ π π ≡ just refl

viewᵉ-diag (`_`with_ {Δ = Δ} x σ)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ˣ_ x
        | viewˢ-diag σ = refl
viewᵉ-diag `true = refl
viewᵉ-diag `false = refl
viewᵉ-diag (`if e₁ `then e₂ `else e₃)
  rewrite viewᵉ-diag e₁
        | viewᵉ-diag e₂
        | viewᵉ-diag e₃ = refl
viewᵉ-diag (`λ⟨ Δ ⟩ e)
  rewrite ≟-diag _≟ᶜ_ Δ
        | viewᵉ-diag e = refl
viewᵉ-diag (_·_ {Δ = Δ} {A = A} e₁ e₂)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ᵗ_ A
        | viewᵉ-diag e₁
        | viewᵉ-diag e₂ = refl
viewᵉ-diag ⟨ e ⟩ 
  rewrite viewᵉ-diag e = refl
viewᵉ-diag (`let⟨_⟩ {A = A} Δ e₁ e₂)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ᵗ_ A
        | viewᵉ-diag e₁
        | viewᵉ-diag e₂ = refl
viewᵉ-diag (`wrap Δ e)
  rewrite ≟-diag _≟ᶜ_ Δ
        | viewᵉ-diag e = refl
viewᵉ-diag (`letwrap {A = A} Δ e₁ e₂)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ᵗ_ A
        | viewᵉ-diag e₁
        | viewᵉ-diag e₂ = refl
viewᵉ-diag (`iflet⟨_⟩ {A = A} {Π = Π} Δ p e₁ e₂ e₃)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ᵗ_ A
        | ≟-diag _≟ᶜ_ Π
        | viewᵖ-diag p
        | viewᵉ-diag e₁
        | viewᵉ-diag e₂
        | viewᵉ-diag e₃ = refl
viewᵉ-diag (`rewritȩ {A = A} {Π = Π} p e₁ e₂)
  rewrite ≟-diag _≟ᵗ_ A
        | ≟-diag _≟ᶜ_ Π
        | viewᵖ-diag p
        | viewᵉ-diag e₁
        | viewᵉ-diag e₂ = refl

viewᵖ-diag `pat = refl
viewᵖ-diag (`_`with₁_ {Δ′ = Δ} x σ)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ˣ_ x
        | viewˢ-diag σ = refl
viewᵖ-diag (`_`with₂_ {Δ′ = Δ} x π)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ˣ_ x
        | viewˢᵖ-diag π = refl
viewᵖ-diag `true = refl
viewᵖ-diag `false = refl
viewᵖ-diag (`if_`then_`else_ {Π₁ = Π₁} {Π₂ = Π₂} {Π₃ = Π₃} p₁ p₂ p₃)
  rewrite ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | ≟-diag _≟ᶜ_ Π₃
        | viewᵖ-diag p₁
        | viewᵖ-diag p₂
        | viewᵖ-diag p₃ = refl
viewᵖ-diag (`λ⟨ Δ′ ⟩ p)
  rewrite ≟-diag _≟ᶜ_ Δ′
        | viewᵖ-diag p = refl
viewᵖ-diag (_·_ {Δ′ = Δ′} {A = A} {Π₁ = Π₁} {Π₂ = Π₂} p₁ p₂)
  rewrite ≟-diag _≟ᶜ_ Δ′
        | ≟-diag _≟ᵗ_ A
        | ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | viewᵖ-diag p₁
        | viewᵖ-diag p₂ = refl
viewᵖ-diag (⟨_⟩ {Π = Π} p)
  rewrite ≟-diag _≟ᶜ_ Π
        | viewᵖ-diag p = refl
viewᵖ-diag (`let⟨_⟩ {A = A} {Π₁ = Π₁} {Π₂ = Π₂} Δ p₁ p₂)
  rewrite ≟-diag _≟ᶜ_ Δ
        | ≟-diag _≟ᵗ_ A
        | ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | viewᵖ-diag p₁
        | viewᵖ-diag p₂ = refl
viewᵖ-diag (`wrap Δ p)
  rewrite ≟-diag _≟ᶜ_ Δ
        | viewᵖ-diag p = refl
viewᵖ-diag (`letwrap {A = A} {Π₁ = Π₁} {Π₂ = Π₂} Δ′ p₁ p₂)
  rewrite ≟-diag _≟ᶜ_ Δ′
        | ≟-diag _≟ᵗ_ A
        | ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | viewᵖ-diag p₁
        | viewᵖ-diag p₂ = refl
viewᵖ-diag (`iflet⟨_⟩ {A = A} {Π = Π} {Π₁ = Π₁} {Π₂ = Π₂} {Π₃ = Π₃} Δ′ p e₁ e₂ e₃)
  rewrite ≟-diag _≟ᶜ_ Δ′
        | ≟-diag _≟ᵗ_ A
        | ≟-diag _≟ᶜ_ Π
        | ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | ≟-diag _≟ᶜ_ Π₃
        | viewᵖ-diag p
        | viewᵖ-diag e₁
        | viewᵖ-diag e₂
        | viewᵖ-diag e₃ = refl
viewᵖ-diag (`rewritȩ {A = A} {Π = Π} {Π₁ = Π₁} {Π₂ = Π₂} p p₁ p₂)
  rewrite ≟-diag _≟ᵗ_ A
        | ≟-diag _≟ᶜ_ Π
        | ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | viewᵖ-diag p
        | viewᵖ-diag p₁
        | viewᵖ-diag p₂ = refl

viewˢ-diag ∅ = refl
viewˢ-diag (σ , term e)
  rewrite viewᵉ-diag e
        | viewˢ-diag σ = refl
viewˢ-diag (σ , var x)
  rewrite ≟-diag _≟ˣ_ x
        | viewˢ-diag σ = refl

viewˢᵖ-diag ∅ = refl
viewˢᵖ-diag (_,_ {Π₁ = Π₁} {Π₂ = Π₂} π (term p))
  rewrite ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | viewᵖ-diag p
        | viewˢᵖ-diag π = refl
viewˢᵖ-diag (_,_ {Π₁ = Π₁} {Π₂ = Π₂} π (var x))
  rewrite ≟-diag _≟ᶜ_ Π₁
        | ≟-diag _≟ᶜ_ Π₂
        | ≟-diag _≟ˣ_ x
        | viewˢᵖ-diag π = refl


nothing≢just : ∀ {A : Set} {x : A} → ¬ (nothing ≡ just x)
nothing≢just {A} {x} ()

-- Decidable equality follows from `view` and `view-diag`
view-diag⇒≟ : (A : Set) → (view : (x y : A) → Maybe (x ≡ y)) → (view-diag : (x : A) → view x x ≡ just refl) →  DecidableEquality A
view-diag⇒≟ A view view-diag x y with view x y in eq₁
... | just refl = yes refl
... | nothing with eq₂ ← view-diag x = no λ { refl → nothing≢just (trans (sym eq₁) eq₂) }

-- Decidable equalities for terms, substitutions, and patterns

_≟ᵉ_ : DecidableEquality (Term n Γ A)
_≟ᵉ_ {n} {Γ} {A} = view-diag⇒≟ (Term n Γ A) viewᵉ viewᵉ-diag

_≟ᵖ_ : DecidableEquality (Pattern n Γ Δ A Π)
_≟ᵖ_ {n} {Γ} {Δ} {A} {Π} = view-diag⇒≟ (Pattern n Γ Δ A Π) viewᵖ viewᵖ-diag

_≟ˢ_ : DecidableEquality (Subst Γ Γ′)
_≟ˢ_ {Γ = Γ} {Γ′ = Γ′} = view-diag⇒≟ (Subst Γ Γ′) viewˢ viewˢ-diag

_≟ˢᵖ_ : DecidableEquality (Γ ∣ Δ ⊩ Δ′ ↝ Π)
_≟ˢᵖ_ {Γ = Γ} {Δ = Δ} {Δ′ = Δ′} {Π = Π} = view-diag⇒≟ (Γ ∣ Δ ⊩ Δ′ ↝ Π) (viewˢᵖ) viewˢᵖ-diag