import lps.IMLL                  as IMLL
import lps.Linearity             as Linearity
import lps.Linearity.Action      as Action
import lps.Linearity.Consumption as Consumption
import lps.Search.BelongsTo      as BelongsTo

import lib.Context               as Con
module BT  = Con.BelongsTo
module BTT = BT.BelongsTo
open import lib.Maybe
open import lib.Nullary

open import Data.Empty
open import Data.Product hiding (map)
open import Data.Nat as ℕ
open import Function

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

module lps.Search.Calculus (Pr : Set) (_≟_ : (x y : Pr) → Dec (x ≡ y)) where

  module Calculus where

    open Con
    open Context
    open IMLL.Type Pr
    open Linearity.Context Pr
    open Action.Context Pr
    module BTC = BelongsTo.Context Pr _≟_

    infix 3 _⊢_⊣_
    infixl 40 _`⊗ʳ_ _`&ʳ_by_
    data _⊢_⊣_ {γ : Con ty} (Γ : Usage γ) : (σ : ty) (Δ : Usage γ) → Set where
      `κ       : ∀ {Γ′ k} (pr : Γ BTC.∋ k ∈ Γ′) → Γ ⊢ `κ k ⊣ Γ′
      _`⊗ʳ_    : ∀ {σ τ Δ E} (s : Γ ⊢ σ ⊣ Δ) (t : Δ ⊢ τ ⊣ E) → Γ ⊢ σ `⊗ τ ⊣ E
      _`&ʳ_by_ : ∀ {σ τ Δ₁ Δ₂ E} (s : Γ ⊢ σ ⊣ Δ₁) (t : Γ ⊢ τ ⊣ Δ₂)
                   (pr : E ≡ Δ₁ ⊙ Δ₂) → Γ ⊢ σ `& τ ⊣ E

    open Context.Context

    ⊢κ : {γ : Con ty} (k : Pr) {Γ : Usage γ} (pr : Σ[ Γ′ ∈ Usage γ ] Γ BTC.∋ k ∈ Γ′) →
         Σ[ Γ′ ∈ Usage γ ] Γ ⊢ `κ k ⊣ Γ′
    ⊢κ k (Δ , pr) = Δ , `κ pr

    infix 5 _⊢⊣?_
    _⊢⊣?_ : ∀ {γ : Con ty} (Γ : Usage γ) (σ : ty) → Con (Σ[ Γ′ ∈ Usage γ ] Γ ⊢ σ ⊣ Γ′)
    Γ ⊢⊣? `κ k   = map (⊢κ k) $ k BTC.∈? Γ
    Γ ⊢⊣? σ `⊗ τ = Γ ⊢⊣? σ >>= uncurry $ λ Δ prσ →
                   Δ ⊢⊣? τ >>= uncurry $ λ E prτ →
                   return $ E , prσ `⊗ʳ prτ
    Γ ⊢⊣? σ `& τ = Γ ⊢⊣? σ >>= uncurry $ λ Δ₁ prσ →
                   Γ ⊢⊣? τ >>= uncurry $ λ Δ₂ prτ →
                   maybe (uncurry $ λ Δ pr → return $ Δ , prσ `&ʳ prτ by pr) ε (Δ₁ ⊙? Δ₂)

    ⊢⊣?-complete : ∀ {γ : Con ty} {Γ : Usage γ} (σ : ty) {Δ : Usage γ} (pr : Γ ⊢ σ ⊣ Δ) →
                  Σ[ pr ∈ Γ ⊢ σ ⊣ Δ ] (Δ , pr) BT.∈ Γ ⊢⊣? σ
    ⊢⊣?-complete (`κ k)   (`κ pr)             = `κ pr , BTT.map (⊢κ k) (BTC.∈?-complete k _ pr)
    ⊢⊣?-complete (σ `⊗ τ) (pr₁ `⊗ʳ pr₂) with ⊢⊣?-complete σ pr₁ | ⊢⊣?-complete τ pr₂
    ... | tm₁ , bt₁ | tm₂ , bt₂ = tm₁ `⊗ʳ tm₂ , BTT.subst bt₁ (BTT.subst bt₂ BT.zro)
    ⊢⊣?-complete (σ `& τ) (_`&ʳ_by_ {Δ₁ = Δ₁} {Δ₂ = Δ₂} {E = Δ} pr₁ pr₂ mg)
        with ⊢⊣?-complete σ pr₁ | ⊢⊣?-complete τ pr₂ | ⊙?-complete _ _ mg
    ... | tm₁ , bt₁ | tm₂ , bt₂ | C , eq =
        tm₁ `&ʳ tm₂ by C
      , BTT.subst bt₁ (BTT.subst bt₂
          (Eq.subst
          (λ tm → (Δ , tm₁ `&ʳ tm₂ by C) BT.∈ maybe (uncurry $ λ Δ pr → return $ Δ , tm₁ `&ʳ tm₂ by pr) ε tm)
          (Eq.sym eq) BT.zro))

    infix 5 _⊢?_
    _⊢?_ : ∀ {γ : Con ty} (Γ : Usage γ) (σ : ty) → Con (Σ[ Γ′ ∈ Usage γ ] isUsed Γ′ × (Γ ⊢ σ ⊣ Γ′))
    Γ ⊢? σ = Γ ⊢⊣? σ >>= uncurry $ λ Γ′ tm → dec (isUsed? Γ′) (λ U → return $ Γ′ , U , tm) (const ε)

    ⊢?-complete : ∀ {γ : Con ty} {Γ : Usage γ} {σ : ty} {Δ : Usage γ} (prΔ : isUsed Δ) (pr : Γ ⊢ σ ⊣ Δ) →
                  Σ[ pr ∈ Γ ⊢ σ ⊣ Δ ] Σ[ prΔ ∈ isUsed Δ ] (Δ , prΔ , pr) BT.∈ Γ ⊢? σ
    ⊢?-complete {Γ = Γ} {σ = σ} {Δ} prΔ pr with Γ ⊢⊣? σ | ⊢⊣?-complete σ pr | isUsed? Δ | Eq.inspect isUsed? Δ
    ... | ts | (tm′ , bt) | yes U | Eq.[ eq ] =
      tm′ , U ,
      let P = λ d → (Δ , U , tm′) BT.∈ dec d (λ U → return $ Δ , U , tm′) (const ε)
      in BTT.subst bt (Eq.subst P (Eq.sym eq) BT.zro)
    ... | ts | (tm′ , bt) | no ¬U | eq = ⊥-elim $ ¬U prΔ

    ⊢⊣-dec : ∀ {γ : Con ty} (Γ : Usage γ) (σ : ty) → Dec (Σ[ Δ ∈ Usage γ ] isUsed Δ × (Γ ⊢ σ ⊣ Δ))
    ⊢⊣-dec Γ σ with Γ ⊢? σ | ⊢?-complete {Γ = Γ} {σ = σ}
    ... | ε      | cmplt = no (BTT.∈ε-elim ∘ proj₂ ∘ proj₂ ∘ uncurry cmplt ∘ proj₂)
    ... | _ ∙ pr | cmplt = yes pr

  module Soundness where

    module Type where

      open Con
      open Context
      open IMLL Pr
      open IMLL.Type Pr
      open Context.Context

      module Cover where

        open Linearity.Type Pr
        open Linearity.Type.Cover Pr
        open Consumption Pr
        open Consumption.Type.Cover Pr
        open Action.Type.Cover Pr
        open Con.BelongsTo
        open BelongsTo.BelongsTo
        open IMLL.RewriteRules Pr

        mutual

          ¬⊙diffˡ : {a : ty} {S S₁ S₂ A : Cover a} →
                  A ≡ S₁ ⊙ S → S ≡ S₁ ─ S₂ → ⊥
          ¬⊙diffˡ (sym prA) prS                = ¬⊙diffʳ prA prS
          ¬⊙diffˡ (`κ k) ()
          ¬⊙diffˡ (prA `⊗ prB) (prS `⊗ prT)    = ¬⊙diffˡ prA prS
          ¬⊙diffˡ (prA `⊗ prB) (prS `⊗ˡ _)     = ¬⊙diffˡ prA prS
          ¬⊙diffˡ (prA `⊗ prB) (_ `⊗ʳ prT)     = ¬⊙diffˡ prB prT
          ¬⊙diffˡ ([ prA ]`⊗ b) (prS `⊗[ .b ]) = ¬⊙diffˡ prA prS
          ¬⊙diffˡ (a `⊗[ prA ]) ([ .a ]`⊗ prS) = ¬⊙diffˡ prA prS
          ¬⊙diffˡ (a `& b) ()
          ¬⊙diffˡ ] prA [`&] prB [ ()
          ¬⊙diffˡ ] prB [`& ()
          ¬⊙diffˡ `&] prA [ ()
          ¬⊙diffˡ (prA `&[ b ]) (prS `&[ .b ]) = ¬⊙diffˡ prA prS
          ¬⊙diffˡ ([ a ]`& prA) ([ .a ]`& prS) = ¬⊙diffˡ prA prS

          ¬⊙diffʳ : {a : ty} {S S₁ S₂ A : Cover a} →
                  A ≡ S ⊙ S₁ → S ≡ S₁ ─ S₂ → ⊥
          ¬⊙diffʳ (sym prA) prS                = ¬⊙diffˡ prA prS
          ¬⊙diffʳ (`κ k) ()
          ¬⊙diffʳ (prA `⊗ prB) (prS `⊗ prT)    = ¬⊙diffʳ prA prS
          ¬⊙diffʳ (prA `⊗ prB) (prS `⊗ˡ _)     = ¬⊙diffʳ prA prS
          ¬⊙diffʳ (prA `⊗ prB) (_ `⊗ʳ prS)     = ¬⊙diffʳ prB prS
          ¬⊙diffʳ ([ prA ]`⊗ b) (prS `⊗[ .b ]) = ¬⊙diffʳ prA prS
          ¬⊙diffʳ (a `⊗[ prB ]) ([ .a ]`⊗ prT) = ¬⊙diffʳ prB prT
          ¬⊙diffʳ (a `& b) ()
          ¬⊙diffʳ ] prA [`&] prB [ ()
          ¬⊙diffʳ ] prB [`& ()
          ¬⊙diffʳ `&] prA [ ()
          ¬⊙diffʳ (prA `&[ b ]) (prS `&[ .b ]) = ¬⊙diffʳ prA prS
          ¬⊙diffʳ ([ a ]`& prB) ([ .a ]`& prT) = ¬⊙diffʳ prB prT

        ⟦A⊙A⟧ : {a : ty} {A A₁ : Cover a} (s : A ≡ A₁ ⊙ A₁) → A ≡ A₁
        ⟦A⊙A⟧ (sym s) = ⟦A⊙A⟧ s
        ⟦A⊙A⟧ (`κ k) = Eq.refl
        ⟦A⊙A⟧ (s₁ `⊗ s₂) rewrite ⟦A⊙A⟧ s₁ | ⟦A⊙A⟧ s₂ = Eq.refl
        ⟦A⊙A⟧ ([ s ]`⊗ b) rewrite ⟦A⊙A⟧ s = Eq.refl
        ⟦A⊙A⟧ (a `⊗[ s ]) rewrite ⟦A⊙A⟧ s = Eq.refl
        ⟦A⊙A⟧ (a `& b) = Eq.refl
        ⟦A⊙A⟧ (s `&[ b ]) rewrite ⟦A⊙A⟧ s = Eq.refl
        ⟦A⊙A⟧ ([ a ]`& s) rewrite ⟦A⊙A⟧ s = Eq.refl

        ⟦⊙⟧⊢ : (Γ₁ Γ₂ Δ : Con ty) {a σ τ : ty} →
          (E₁ : Cover a) (tm₁ : Γ₁ ++ ｢ E₁ ｣ ++ Δ ⊢ σ)
          (E₂ : Cover a) (tm₂ : Γ₂ ++ ｢ E₂ ｣ ++ Δ ⊢ τ) →
          (E : Cover a) → E ≡ E₁ ⊙ E₂ →
          Γ₁ ++ ｢ E ｣ ++ Δ ⊢ σ × Γ₂ ++ ｢ E ｣ ++ Δ ⊢ τ
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ E₁ tm₁ E₂ tm₂ _ (sym s) =
          let (tm₁ , tm₂) = ⟦⊙⟧⊢ Γ₂ Γ₁ Δ E₂ tm₂ E₁ tm₁ _ s
          in tm₂ , tm₁
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ .(`κ k) tm₁ .(`κ k) tm₂ ._ (`κ k) = tm₁ , tm₂
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ (S₁ `⊗ T₁) tm₁ (S₂ `⊗ T₂) tm₂ (S `⊗ T) (s₁ `⊗ s₂) =
          let (tm₁ , tm₂) = ⟦⊙⟧⊢ (Γ₁ ++ ｢ S₁ ｣) (Γ₂ ++ ｢ S₂ ｣) Δ
                   T₁ (tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ tm₁)
                   T₂ (tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ tm₂)
                   T s₂
              (tm₁ , tm₂) = ⟦⊙⟧⊢ Γ₁ Γ₂ (｢ T ｣ ++ Δ)
                   S₁ (tm-assoc (Γ₁ ++ ｢ S₁ ｣) ｢ T ｣ Δ tm₁)
                   S₂ (tm-assoc (Γ₂ ++ ｢ S₂ ｣) ｢ T ｣ Δ tm₂)
                   S s₁
          in (tm-group Γ₁ ｢ S ｣ ｢ T ｣ Δ $ tm-assoc⁻¹ (Γ₁ ++ ｢ S ｣) ｢ T ｣ Δ tm₁)
           , (tm-group Γ₂ ｢ S ｣ ｢ T ｣ Δ $ tm-assoc⁻¹ (Γ₂ ++ ｢ S ｣) ｢ T ｣ Δ tm₂)
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ ._ tm₁ ._ tm₂ ._ ([ s ]`⊗ b) = ⟦⊙⟧⊢ Γ₁ Γ₂ Δ _ tm₁ _ tm₂ _ s
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ ._ tm₁ ._ tm₂ ._ (a `⊗[ s ]) = ⟦⊙⟧⊢ Γ₁ Γ₂ Δ _ tm₁ _ tm₂ _ s
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ .(a `& b) tm₁ .(a `& b) tm₂ ._ (a `& b) = tm₁ , tm₂
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ ._ tm₁ ._ tm₂ ._ ] prA [`&] prB [ =
            ⟦isUsed⟧ Γ₁ Δ (prA `&[ _ ]) tm₁
          , ⟦isUsed⟧ Γ₂ Δ ([ _ ]`& prB) tm₂
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ ._ tm₁ ._ tm₂ ._ ] prB [`& = ⟦isUsed⟧ Γ₁ Δ ([ _ ]`& prB) tm₁ , tm₂
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ ._ tm₁ ._ tm₂ ._ `&] prA [ = ⟦isUsed⟧ Γ₁ Δ (prA `&[ _ ]) tm₁ , tm₂
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ ._ tm₁ ._ tm₂ ._ (s `&[ b ]) = ⟦⊙⟧⊢ Γ₁ Γ₂ Δ _ tm₁ _ tm₂ _ s
        ⟦⊙⟧⊢ Γ₁ Γ₂ Δ ._ tm₁ ._ tm₂ ._ ([ a ]`& s) = ⟦⊙⟧⊢ Γ₁ Γ₂ Δ _ tm₁ _ tm₂ _ s


        ⟦⊙⟧─ : {a : ty} {A B₁ B₂ : Cover a} →
            (E₁ : Cover a) (d₁ : B₁ ≡ A ─ E₁) (E₂ : Cover a) (d₂ : B₂ ≡ A ─ E₂) →
            {B : Cover a} → B ≡ B₁ ⊙ B₂ → Σ[ E ∈ Cover a ] B ≡ A ─ E × E ≡ E₁ ⊙ E₂
        ⟦⊙⟧─ E₁ d₁ E₂ d₂ (sym s) = let (E , d , s) = ⟦⊙⟧─ E₂ d₂ E₁ d₁ s in E , d , sym s
        ⟦⊙⟧─ ._ (d₁ `⊗ d₂) ._ (d₃ `⊗ d₄) (s₁ `⊗ s₂) =
          let (F₁ , d₁ , s₁) = ⟦⊙⟧─ _ d₁ _ d₃ s₁
              (F₂ , d₂ , s₂) = ⟦⊙⟧─ _ d₂ _ d₄ s₂
          in F₁ `⊗ F₂ , d₁ `⊗ d₂ , s₁ `⊗ s₂
        ⟦⊙⟧─ ._ (d₁ `⊗ˡ B₁) ._ (d₂ `⊗ˡ .B₁) (s₁ `⊗ s₂) =
          let (E , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s₁
          in E `⊗[ _ ]
           , Eq.subst (λ B → _ `⊗ B ≡ _ `⊗ _ ─ E `⊗[ _ ]) (Eq.sym $ ⟦A⊙A⟧ s₂) (d `⊗ˡ B₁)
           , [ s ]`⊗ _
        ⟦⊙⟧─ ._ (A₂ `⊗ʳ d₁) ._ (.A₂ `⊗ʳ d₂) (s₁ `⊗ s₂) =
          let (E , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s₂
          in [ _ ]`⊗ E
           , Eq.subst (λ B → B `⊗ _ ≡ _ `⊗ _ ─ [ _ ]`⊗ E) (Eq.sym $ ⟦A⊙A⟧ s₁) (A₂ `⊗ʳ d)
           , _ `⊗[ s ]
        ⟦⊙⟧─ ._ ([ A₁ ]`⊗ˡ B₁) ._ ([ A₂ ]`⊗ˡ .B₁) {A `⊗ B} (s₁ `⊗ s₂) =
             A `⊗[ _ ]
           , Eq.subst (λ B → _ `⊗ B ≡ [ _ ]`⊗ _ ─ A `⊗[ _ ])
                      (Eq.sym $ ⟦A⊙A⟧ s₂) ([ A ]`⊗ˡ B₁)
           , [ s₁ ]`⊗ _
        ⟦⊙⟧─ ._ ([ A₁ ]`⊗ˡʳ d₁) ._ ([ A₂ ]`⊗ˡʳ d₂) {A `⊗ B} (s₁ `⊗ s₂) =
           let (B , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s₂
           in A `⊗ B , [ A ]`⊗ˡʳ d , s₁ `⊗ s
        ⟦⊙⟧─ ._ (A₁ `⊗ʳ[ B₁ ]) ._ (.A₁ `⊗ʳ[ B₂ ]) {A `⊗ B} (s₁ `⊗ s₂) =
             [ _ ]`⊗ B 
           , Eq.subst (λ A → A `⊗ _ ≡ _ `⊗[ _ ] ─ [ _ ]`⊗ B)
                      (Eq.sym $ ⟦A⊙A⟧ s₁) (A₁ `⊗ʳ[ B ])
           , _ `⊗[ s₂ ]
        ⟦⊙⟧─ ._ (d₁ `⊗ˡʳ[ B₁ ]) ._ (d₂ `⊗ˡʳ[ B₂ ]) {A `⊗ B} (s₁ `⊗ s₂) =
           let (A , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s₁
           in A `⊗ B , d `⊗ˡʳ[ B ] , s `⊗ s₂
        ⟦⊙⟧─ ._ (d₁ `⊗[ b ]) ._ (d₂ `⊗[ .b ]) ([ s ]`⊗ .b) =
          let (E , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s
          in E `⊗[ b ] , d `⊗[ b ] , [ s ]`⊗ b
        ⟦⊙⟧─ ._ ([ σ ]`⊗ d₁) ._ ([ .σ ]`⊗ d₂) (.σ `⊗[ s ]) =
          let (E , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s
          in [ σ ]`⊗ E , [ σ ]`⊗ d , σ `⊗[ s ]
        ⟦⊙⟧─ E₁ () ._ ([ σ ]`& d₂) ] prA [`&] prB [
        ⟦⊙⟧─ E₁ d₁ E₂ () ] prB [`&
        ⟦⊙⟧─ E₁ d₁ E₂ () `&] prA [
        ⟦⊙⟧─ ._ (d₁ `&[ b ]) ._ (d₂ `&[ .b ]) (s `&[ .b ]) =
           let (E , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s
           in E `&[ b ] , d `&[ b ] , s `&[ b ]
        ⟦⊙⟧─ ._ ([ σ ]`& d₁) ._ ([ .σ ]`& d₂) ([ .σ ]`& s) =
           let (E , d , s) = ⟦⊙⟧─ _ d₁ _ d₂ s
           in [ σ ]`& E , [ σ ]`& d , [ σ ]`& s
        ⟦⊙⟧─ E₁ () E₂ d₂ (`κ k)
        ⟦⊙⟧─ E₁ () E₂ d₂ (a `& b)
        ⟦⊙⟧─ ._ (_  `⊗ d₂) ._ (_ `⊗ˡ _) (_ `⊗ s₂) = ⊥-elim $ ¬⊙diffʳ s₂ d₂
        ⟦⊙⟧─ ._ (d₁ `⊗ d₂) ._ (_ `⊗ʳ _) (s₁ `⊗ _) = ⊥-elim $ ¬⊙diffʳ s₁ d₁
        ⟦⊙⟧─ ._ (_ `⊗ˡ _) ._ (_ `⊗ d₃) (_ `⊗ s₂)  = ⊥-elim $ ¬⊙diffˡ s₂ d₃
        ⟦⊙⟧─ ._ (_ `⊗ˡ _) ._ (_ `⊗ʳ d₂) (_ `⊗ s₂) = ⊥-elim $ ¬⊙diffˡ s₂ d₂
        ⟦⊙⟧─ ._ (_ `⊗ʳ _) ._ (d₂ `⊗ _) (s₁ `⊗ _)  = ⊥-elim $ ¬⊙diffˡ s₁ d₂
        ⟦⊙⟧─ ._ (_ `⊗ʳ _) ._ (d₂ `⊗ˡ _) (s₁ `⊗ _) = ⊥-elim $ ¬⊙diffˡ s₁ d₂
        ⟦⊙⟧─ ._ ([ _ ]`⊗ˡ _) ._ ([ _ ]`⊗ˡʳ d₂) (_ `⊗ s₂) = ⊥-elim $ ¬⊙diffˡ s₂ d₂
        ⟦⊙⟧─ ._ (_ `⊗ʳ[ _ ]) ._ (d₂ `⊗ˡʳ[ _ ]) (s₁ `⊗ _) = ⊥-elim $ ¬⊙diffˡ s₁ d₂
        ⟦⊙⟧─ ._ ([ _ ]`⊗ˡʳ d₁) ._ ([ _ ]`⊗ˡ _) (_ `⊗ s₂) = ⊥-elim $ ¬⊙diffʳ s₂ d₁
        ⟦⊙⟧─ ._ (d₁ `⊗ˡʳ[ _ ]) ._ (_ `⊗ʳ[ _ ]) (s₁ `⊗ _) = ⊥-elim $ ¬⊙diffʳ s₁ d₁

        ⟦⊙⟧ : (Γ₁ Γ₂ Δ : Con ty) {a σ τ : ty} {A B₁ B₂ : Cover a} →
          (E₁ : Cover a) (d₁ : B₁ ≡ A ─ E₁) (tm₁ : Γ₁ ++ ｢ E₁ ｣ ++ Δ ⊢ σ)
          (E₂ : Cover a) (d₂ : B₂ ≡ A ─ E₂) (tm₂ : Γ₂ ++ ｢ E₂ ｣ ++ Δ ⊢ τ) →
          {B : Cover a} → B ≡ B₁ ⊙ B₂ →
          Σ[ E ∈ Cover a ] B ≡ A ─ E × Γ₁ ++ ｢ E ｣ ++ Δ ⊢ σ × Γ₂ ++ ｢ E ｣ ++ Δ ⊢ τ
        ⟦⊙⟧ Γ₁ Γ₂ Δ E₁ d₁ tm₁ E₂ d₂ tm₂ s =
          let (E , d , s) = ⟦⊙⟧─ E₁ d₁ E₂ d₂ s
              (tm₁ , tm₂) = ⟦⊙⟧⊢ Γ₁ Γ₂ Δ E₁ tm₁ E₂ tm₂ E s
          in E , d , tm₁ , tm₂

        open Interleaving

        ｢─｣ : {a : ty} {S S₁ S₂ : Cover a} (d : S ≡ S₁ ─ S₂) → ｢ S ｣ ≡ ｢ S₁ ｣ ⋈ ｢ S₂ ｣
        ｢─｣ (d₁ `⊗ d₂)    = ｢─｣ d₁ Interleaving.++ ｢─｣ d₂
        ｢─｣ ([ σ ]`⊗ d)   = ｢─｣ d
        ｢─｣ (d `⊗[ τ ])   = ｢─｣ d
        ｢─｣ ([ σ ]`& d)   = ｢─｣ d
        ｢─｣ (d `&[ τ ])   = ｢─｣ d
        ｢─｣ (d `⊗ˡ T)     = ｢─｣ d Interleaving.++ˡ ｢ T ｣
        ｢─｣ (S `⊗ʳ d)     = ｢ S ｣ Interleaving.ˡ++ ｢─｣ d
        ｢─｣ ([ S ]`⊗ˡ T)  = ｢ S ｣ Interleaving.ʳ++ˡ ｢ T ｣
        ｢─｣ ([ S ]`⊗ˡʳ d) = ｢ S ｣ Interleaving.ʳ++ ｢─｣ d
        ｢─｣ (S `⊗ʳ[ T ])  = ｢ S ｣ Interleaving.ˡ++ʳ ｢ T ｣
        ｢─｣ (d `⊗ˡʳ[ T ]) = ｢─｣ d Interleaving.++ʳ ｢ T ｣

        ⟦>>=⟧ : {σ : ty} {S T U : Cover σ} (Γ₁ Δ₁ Γ₂ Δ₂ : Con ty) {a b : ty}
             (V₁ : Cover σ) (d₁ : T ≡ S ─ V₁) (tm₁ : Γ₁ ++ ｢ V₁ ｣ ++ Δ₁ ⊢ a)
             (V₂ : Cover σ) (d₂ : U ≡ T ─ V₂) (tm₂ : Γ₂ ++ ｢ V₂ ｣ ++ Δ₂ ⊢ b) →
             Σ[ V ∈ Cover σ ] Σ[ S₁ ∈ Con ty ] Σ[ S₂ ∈ Con ty ]
               U ≡ S ─ V × ｢ V ｣ ≡ S₁ ⋈ S₂
             × Γ₁ ++ S₁ ++ Δ₁ ⊢ a × Γ₂ ++ S₂ ++ Δ₂ ⊢ b
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ ([ σ ]`& d₁) tm₁ ._ ([ .σ ]`& d₂) tm₂ =
          let (T , T₁ , T₂ , d , j , tms) = ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ _ d₁ tm₁ _ d₂ tm₂
          in [ σ ]`& T , T₁ , T₂ , [ σ ]`& d , j , tms
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ (d₁ `&[ τ ]) tm₁ ._ (d₂ `&[ .τ ]) tm₂ =
          let (S , S₁ , S₂ , d , j , tms) = ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ _ d₁ tm₁ _ d₂ tm₂
          in S `&[ τ ] , S₁ , S₂ , d `&[ τ ] , j , tms
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗ T₁) (d₁ `⊗ d₃) tm₁ (S₂ `⊗ T₂) (d₂ `⊗ d₄) tm₂ =
          let (T , T₁ , T₂ , dT , jT , tm₁ , tm₂) =
                ⟦>>=⟧ (Γ₁ ++ ｢ S₁ ｣) Δ₁ (Γ₂ ++ ｢ S₂ ｣) Δ₂ _ d₃
                (tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ₁ tm₁) _ d₄
                (tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ₂ tm₂)
              (S , S₁ , S₂ , dS , jS , tm₁ , tm₂) =
                ⟦>>=⟧ Γ₁ (T₁ ++ Δ₁) Γ₂ (T₂ ++ Δ₂) _ d₁
                (tm-assoc (Γ₁ ++ ｢ S₁ ｣) T₁ Δ₁ tm₁) _ d₂
                (tm-assoc (Γ₂ ++ ｢ S₂ ｣) T₂ Δ₂ tm₂)
          in S `⊗ T , S₁ ++ T₁ , S₂ ++ T₂ , dS `⊗ dT , jS Interleaving.++ jT ,
             tm-group Γ₁ S₁ T₁ Δ₁ (tm-assoc⁻¹ (Γ₁ ++ S₁) T₁ Δ₁ tm₁)
           , tm-group Γ₂ S₂ T₂ Δ₂ (tm-assoc⁻¹ (Γ₂ ++ S₂) T₂ Δ₂ tm₂)
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗ T₁) (d₁ `⊗ d₂) tm₁ (S₂ `⊗[ τ ]) (d₃ `⊗ˡ T) tm₂ =
          let tm₁ = tm-assoc (Γ₁ ++ ｢ S₁ ｣) ｢ T₁ ｣ Δ₁ $
                      tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ₁ tm₁
              (S , S₁ , S₂ , d , j , tm₁ , tm₂) =
                ⟦>>=⟧ Γ₁ (｢ T₁ ｣ ++ Δ₁) Γ₂ Δ₂ S₁ d₁ tm₁ S₂ d₃ tm₂
          in S `⊗ T₁ , S₁ ++ ｢ T₁ ｣ , S₂ , d `⊗ d₂ , j Interleaving.++ˡ ｢ T₁ ｣
           , (tm-group Γ₁ S₁ ｢ T₁ ｣ Δ₁ $ tm-assoc⁻¹ (Γ₁ ++ S₁) ｢ T₁ ｣ Δ₁ tm₁) , tm₂ 
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗ T₁) (d₁ `⊗ d₂) tm₁ ([ σ ]`⊗ T₂) (S `⊗ʳ d₃) tm₂ =
          let tm₁ = tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ₁ tm₁
              (T , T₁ , T₂ , d , j , tm₁ , tm₂) =
                ⟦>>=⟧ (Γ₁ ++ ｢ S₁ ｣) Δ₁ Γ₂ Δ₂ T₁ d₂ tm₁ T₂ d₃ tm₂
          in S₁ `⊗ T , ｢ S₁ ｣ ++ T₁ , T₂ , d₁ `⊗ d , ｢ S₁ ｣ Interleaving.ˡ++ j
           , tm-group Γ₁ ｢ S₁ ｣ T₁ Δ₁ tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ ([ σ ]`⊗ d₁) tm₁ ._ ([ .σ ]`⊗ d₂) tm₂ = 
          let (T , T₁ , T₂ , d , j , tms) = ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ _ d₁ tm₁ _ d₂ tm₂
          in [ σ ]`⊗ T , T₁ , T₂ , [ σ ]`⊗ d , j , tms
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ([ σ ]`⊗ T₁) ([ .σ ]`⊗ d₁) tm₁
                         (.S₂ `⊗[ τ ]) ([ S₂ ]`⊗ˡ T₂) tm₂ =
           S₂ `⊗ T₁ , ｢ T₁ ｣ , ｢ S₂ ｣ , [ S₂ ]`⊗ˡʳ d₁
         , ｢ S₂ ｣ Interleaving.ʳ++ˡ ｢ T₁ ｣ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ([ .σ ]`⊗ T₁) ([ σ ]`⊗ d₁) tm₁
                         (.S₂ `⊗ T₂) ([ S₂ ]`⊗ˡʳ d₂) tm₂ =
          let (T , T₁ , T₂ , d , j , tm₁ , tm₂) =
                ⟦>>=⟧ Γ₁ Δ₁ (Γ₂ ++ ｢ S₂ ｣) Δ₂ T₁ d₁ tm₁ T₂ d₂ $
                tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ₂ tm₂
          in S₂ `⊗ T , T₁ , ｢ S₂ ｣ ++ T₂ , [ S₂ ]`⊗ˡʳ d
           , ｢ S₂ ｣ Interleaving.ʳ++ j , tm₁ , tm-group Γ₂ ｢ S₂ ｣ T₂ Δ₂ tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ (d₁ `⊗[ τ ]) tm₁ ._ (d₂ `⊗[ .τ ]) tm₂ =
          let (S , S₁ , S₂ , d , j , tms) = ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ _ d₁ tm₁ _ d₂ tm₂
          in S `⊗[ τ ] , S₁ , S₂ , d `⊗[ τ ] , j , tms
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗[ .τ ]) (d₁ `⊗[ τ ]) tm₁
                         ([ σ ]`⊗ .T₂) (S₂ `⊗ʳ[ T₂ ]) tm₂ =
            S₁ `⊗ T₂ , ｢ S₁ ｣ , ｢ T₂ ｣ , d₁ `⊗ˡʳ[ T₂ ]
          , ｢ S₁ ｣ Interleaving.ˡ++ʳ ｢ T₂ ｣ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗[ .τ ]) (d₁ `⊗[ τ ]) tm₁
                         (S₂ `⊗ .T₂) (d₂ `⊗ˡʳ[ T₂ ]) tm₂ =
           let tm₂ = tm-assoc (Γ₂ ++ ｢ S₂ ｣) ｢ T₂ ｣ Δ₂ $
                     tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ₂ tm₂
               (S , S₁ , S₂ , d , j , tm₁ , tm₂) =
                 ⟦>>=⟧ Γ₁ Δ₁ Γ₂ (｢ T₂ ｣ ++ Δ₂) _ d₁ tm₁ _ d₂ tm₂
           in S `⊗ T₂ , S₁ , S₂ ++ ｢ T₂ ｣ , d `⊗ˡʳ[ T₂ ] ,
             j Interleaving.++ Interleaving.reflʳ {Γ = ｢ T₂ ｣} , tm₁
           , (tm-group Γ₂ S₂ ｢ T₂ ｣ Δ₂ $ tm-assoc⁻¹ (Γ₂ ++ S₂) ｢ T₂ ｣ Δ₂ tm₂)
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗[ τ ]) (d₁ `⊗ˡ T) tm₁ (S₂ `⊗ T₂) (d₂ `⊗ d₃) tm₂ =
          let tm₂ = tm-assoc (Γ₂ ++ ｢ S₂ ｣) ｢ T₂ ｣ Δ₂ $
                    tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ₂ tm₂
              (S , S₁ , S₂ , d , j , tm₁ , tm₂) =
                ⟦>>=⟧ Γ₁ Δ₁ Γ₂ (｢ T₂ ｣ ++ Δ₂) S₁ d₁ tm₁ S₂ d₂ tm₂
          in S `⊗ T₂ , S₁ , S₂ ++ ｢ T₂ ｣ , d `⊗ d₃ , j Interleaving.++ʳ ｢ T₂ ｣
           , tm₁ , (tm-group Γ₂ S₂ ｢ T₂ ｣ Δ₂ $ tm-assoc⁻¹ (Γ₂ ++ S₂) ｢ T₂ ｣ Δ₂ tm₂)
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ (d₁ `⊗ˡ T) tm₁ ._ (d₂ `⊗ˡ .T) tm₂ =
          let (S , S₁ , S₂ , d , jtms) = ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ _ d₁ tm₁ _ d₂ tm₂
          in S `⊗[ _ ] , S₁ , S₂ , d `⊗ˡ T , jtms
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗[ τ ]) (d₁ `⊗ˡ T) tm₁ ([ σ ]`⊗ T₂) (S `⊗ʳ d₂) tm₂ =
            S₁ `⊗ T₂ , ｢ S₁ ｣ , ｢ T₂ ｣ , d₁ `⊗ d₂ , ｢ S₁ ｣ Interleaving.ˡ++ʳ ｢ T₂ ｣
          , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ([ σ ]`⊗ T₁) (S `⊗ʳ d₁) tm₁ (S₂ `⊗ T₂) (d₂ `⊗ d₃) tm₂ =
          let (T , T₁ , T₂ , d , j , tm₁ , tm₂) =
                ⟦>>=⟧ Γ₁ Δ₁ (Γ₂ ++ ｢ S₂ ｣) Δ₂ T₁ d₁ tm₁ T₂ d₃ $
                tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ₂ tm₂
          in S₂ `⊗ T , T₁ , ｢ S₂ ｣ ++ T₂ , d₂ `⊗ d , ｢ S₂ ｣ Interleaving.ʳ++ j
           , tm₁ , tm-group Γ₂ ｢ S₂ ｣ T₂ Δ₂ tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ([ σ ]`⊗ T₁) (S `⊗ʳ d₁) tm₁ (S₂ `⊗[ τ ]) (d₂ `⊗ˡ T) tm₂ =
            S₂ `⊗ T₁ , ｢ T₁ ｣ , ｢ S₂ ｣ , d₂ `⊗ d₁ , ｢ S₂ ｣ Interleaving.ʳ++ˡ ｢ T₁ ｣
          , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ (S `⊗ʳ d₁) tm₁ ._ (.S `⊗ʳ d₂) tm₂ = 
          let (T , T₁ , T₂ , d , jtms) = ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ _ d₁ tm₁ _ d₂ tm₂
          in [ _ ]`⊗ T , T₁ , T₂ , S `⊗ʳ d , jtms
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (.S₁ `⊗[ τ ]) ([ S₁ ]`⊗ˡ T) tm₁ (S₂ `⊗ T₂) (d₂ `⊗ d₃) tm₂ =
          _ `⊗ T₂ , ｢ S₁ ｣ , ｢ S₂ ｣ ++ ｢ T₂ ｣ , [ _ ]`⊗ˡʳ d₃ , ｢─｣ d₂ Interleaving.++ʳ ｢ T₂ ｣ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (.S₁ `⊗[ τ ]) ([ S₁ ]`⊗ˡ T) tm₁ (S₂ `⊗[ .τ ]) (d₂ `⊗ˡ .T) tm₂ =
           _ , ｢ S₁ ｣ , ｢ S₂ ｣ , [ _ ]`⊗ˡ T , ｢─｣ d₂ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (.S₁ `⊗[ τ ]) ([ S₁ ]`⊗ˡ T₁) tm₁ ([ σ ]`⊗ T₂) (.S₁ `⊗ʳ d₂) tm₂ =
          S₁ `⊗ T₂ , ｢ S₁ ｣ , ｢ T₂ ｣ , [ _ ]`⊗ˡʳ d₂ , ｢ S₁ ｣ Interleaving.ˡ++ʳ ｢ T₂ ｣ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (.S₁ `⊗ T₁) ([ S₁ ]`⊗ˡʳ d₁) tm₁ (S₂ `⊗ T₂) (d₂ `⊗ d₃) tm₂ =
          let tm₁ = tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ₁ tm₁
              tm₂ = tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ₂ tm₂
              (T , T₁ , T₂ , dT , jT , tm₁ , tm₂) = ⟦>>=⟧ (Γ₁ ++ ｢ S₁ ｣) Δ₁ (Γ₂ ++ ｢ S₂ ｣) Δ₂ T₁ d₁ tm₁ T₂ d₃ tm₂
          in _ `⊗ T , ｢ S₁ ｣ ++ T₁ , ｢ S₂ ｣ ++ T₂ , [ _ ]`⊗ˡʳ dT , ｢─｣ d₂ Interleaving.++ jT
           , tm-group Γ₁ ｢ S₁ ｣ T₁ Δ₁ tm₁ , tm-group Γ₂ ｢ S₂ ｣ T₂ Δ₂ tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (.S₁ `⊗ T₁) ([ S₁ ]`⊗ˡʳ d₁) tm₁ (S₂ `⊗[ τ ]) (d₂ `⊗ˡ T) tm₂ =
           _ `⊗ T₁ , ｢ S₁ ｣ ++ ｢ T₁ ｣ , ｢ S₂ ｣ , [ _ ]`⊗ˡʳ d₁ , ｢─｣ d₂ Interleaving.++ˡ ｢ T₁ ｣ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (.S₁ `⊗ T₁) ([ S₁ ]`⊗ˡʳ d₁) tm₁
                         ([ σ ]`⊗ T₂) (.S₁ `⊗ʳ d₂) tm₂ =
          let tm₁ = tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ₁ tm₁
              (T , T₁ , T₂ , d , j , tm₁ , tm₂) =
                ⟦>>=⟧ (Γ₁ ++ ｢ S₁ ｣) Δ₁ Γ₂ Δ₂ T₁ d₁ tm₁ T₂ d₂ tm₂
          in S₁ `⊗ T , ｢ S₁ ｣ ++ T₁ , T₂ , [ S₁ ]`⊗ˡʳ d
           , ｢ S₁ ｣ Interleaving.ˡ++ j , tm-group Γ₁ ｢ S₁ ｣ T₁ Δ₁ tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ([ σ ]`⊗ .T₁) (S `⊗ʳ[ T₁ ]) tm₁ (S₂ `⊗ T₂) (d₂ `⊗ d₃) tm₂ =
          S₂ `⊗ _ , ｢ T₁ ｣ , ｢ S₂ ｣ ++ ｢ T₂ ｣ , d₂ `⊗ˡʳ[ _ ] , ｢ S₂ ｣ Interleaving.ʳ++ ｢─｣ d₃ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ([ σ ]`⊗ .T₁) (S `⊗ʳ[ T₁ ]) tm₁
                         (S₂ `⊗[ τ ]) (d₂ `⊗ˡ .T₁) tm₂ =
            S₂ `⊗ T₁ , ｢ T₁ ｣ , ｢ S₂ ｣ , d₂ `⊗ˡʳ[ T₁ ]
          , ｢ S₂ ｣ Interleaving.ʳ++ˡ ｢ T₁ ｣ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ([ σ ]`⊗ .T₁) (S `⊗ʳ[ T₁ ]) tm₁ ([ .σ ]`⊗ T₂) (.S `⊗ʳ d₂) tm₂ =
          [ σ ]`⊗ _ , ｢ T₁ ｣ , ｢ T₂ ｣ , S `⊗ʳ[ _ ] , ｢─｣ d₂ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗ .T₁) (d₁ `⊗ˡʳ[ T₁ ]) tm₁ (S₂ `⊗ T₂) (d₂ `⊗ d₃) tm₂ =
          let tm₁ = tm-assoc (Γ₁ ++ ｢ S₁ ｣) ｢ T₁ ｣ Δ₁ $ tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ₁ tm₁
              tm₂ = tm-assoc (Γ₂ ++ ｢ S₂ ｣) ｢ T₂ ｣ Δ₂ $ tm-group⁻¹ Γ₂ ｢ S₂ ｣ ｢ T₂ ｣ Δ₂ tm₂
              (S , S₁ , S₂ , dS , jS , tm₁ , tm₂) = ⟦>>=⟧ Γ₁ (｢ T₁ ｣ ++ Δ₁) Γ₂ (｢ T₂ ｣ ++ Δ₂) S₁ d₁ tm₁ S₂ d₂ tm₂
          in S `⊗ _ , S₁ ++ ｢ T₁ ｣ , S₂ ++ ｢ T₂ ｣ , dS `⊗ˡʳ[ _ ] , jS Interleaving.++ ｢─｣ d₃
           , (tm-group Γ₁ S₁ ｢ T₁ ｣ Δ₁ $ tm-assoc⁻¹ (Γ₁ ++ S₁) ｢ T₁ ｣ Δ₁ tm₁)
           , (tm-group Γ₂ S₂ ｢ T₂ ｣ Δ₂ $ tm-assoc⁻¹ (Γ₂ ++ S₂) ｢ T₂ ｣ Δ₂ tm₂)
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗ .T₁) (d₁ `⊗ˡʳ[ T₁ ]) tm₁
                         (S₂ `⊗[ τ ]) (d₂ `⊗ˡ .T₁) tm₂ =
          let tm₁ = tm-assoc (Γ₁ ++ ｢ S₁ ｣) ｢ T₁ ｣ Δ₁ $
                    tm-group⁻¹ Γ₁ ｢ S₁ ｣ ｢ T₁ ｣ Δ₁ tm₁
              (S , S₁ , S₂ , d , j , tm₁ , tm₂) = 
                ⟦>>=⟧ Γ₁ (｢ T₁ ｣ ++ Δ₁) Γ₂ Δ₂ S₁ d₁ tm₁ S₂ d₂ tm₂
          in S `⊗ T₁ , S₁ ++ ｢ T₁ ｣ , S₂ , d `⊗ˡʳ[ T₁ ] , j Interleaving.++ˡ ｢ T₁ ｣
           , (tm-group Γ₁ S₁ ｢ T₁ ｣ Δ₁ $ tm-assoc⁻¹ (Γ₁ ++ S₁) ｢ T₁ ｣ Δ₁ tm₁) , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ (S₁ `⊗ .T₁) (d₁ `⊗ˡʳ[ T₁ ]) tm₁ ([ σ ]`⊗ T₂) (S `⊗ʳ d₂) tm₂ =
          S₁ `⊗ _ , ｢ S₁ ｣ ++ ｢ T₁ ｣ , ｢ T₂ ｣ , d₁ `⊗ˡʳ[ _ ] , ｢ S₁ ｣ Interleaving.ˡ++ ｢─｣ d₂ , tm₁ , tm₂

      module Usage where

        open Linearity.Type Pr
        open Linearity.Type.Usage Pr
        open Consumption.Type.Usage Pr
        open Action.Type.Usage Pr

        ⟦⊙⟧ : (Γ₁ Γ₂ Δ : Con ty) {a σ τ : ty} {A : Usage a} {B₁ B₂ : Usage a} →
              (E₁ : Usage a) (d₁ : B₁ ≡ A ─ E₁) (tm₁ : Γ₁ ++ ｢ E₁ ｣ ++ Δ ⊢ σ) 
              (E₂ : Usage a) (d₂ : B₂ ≡ A ─ E₂) (tm₂ : Γ₂ ++ ｢ E₂ ｣ ++ Δ ⊢ τ)
              {B : Usage a} → B ≡ B₁ ⊙ B₂ →
              Σ[ E ∈ Usage a ] B ≡ A ─ E ×
              Γ₁ ++ ｢ E ｣ ++ Δ ⊢ σ × Γ₂ ++ ｢ E ｣ ++ Δ ⊢ τ
        ⟦⊙⟧ Γ₁ Γ₂ Δ .([ a ]) `idˡ tm₁ .([ a ]) `idˡ tm₂ [ a ] = [ a ] , `idˡ , tm₁ , tm₂
        ⟦⊙⟧ Γ₁ Γ₂ Δ .([ a ]) `idˡ tm₁ .([ a ]) `idʳ tm₂ [ a ] = [ a ] , `idˡ , tm₁ , tm₂
        ⟦⊙⟧ Γ₁ Γ₂ Δ .([ a ]) `idʳ tm₁ .([ a ]) `idˡ tm₂ [ a ] = [ a ] , `idˡ , tm₁ , tm₂
        ⟦⊙⟧ Γ₁ Γ₂ Δ .([ a ]) `idʳ tm₁ .([ a ]) `idʳ tm₂ [ a ] = [ a ] , `idˡ , tm₁ , tm₂
        ⟦⊙⟧ Γ₁ Γ₂ Δ ._ `idˡ tm₁ ._ `idˡ tm₂ ] prA [ = [ _ ] , pr , tm₁ , tm₂
          where pr = Eq.subst (λ A → ] _ [ ≡ ] A [ ─ [ _ ]) (Cover.⟦A⊙A⟧ prA) `idˡ
        ⟦⊙⟧ Γ₁ Γ₂ Δ ._ `idʳ tm₁ ._ `idʳ tm₂ ] prA [ =
          ] _ [ , `idʳ , Cover.⟦⊙⟧⊢ Γ₁ Γ₂ Δ _ tm₁ _ tm₂ _ prA
        ⟦⊙⟧ Γ₁ Γ₂ Δ ._ ] prS₁ [ tm₁ ._ ] prS₂ [ tm₂ ] prA [ =
          let (S , prS , tms) = Cover.⟦⊙⟧ Γ₁ Γ₂ Δ _ prS₁ tm₁ _ prS₂ tm₂ prA
          in ] S [ , ] prS [ , tms
        ⟦⊙⟧ _ _ _ ._ `idˡ _ ._ ] prS [ _ ] prA [ = ⊥-elim $ Cover.¬⊙diffˡ prA prS
        ⟦⊙⟧ _ _ _ ._ ] prS [ _ ._ `idˡ _ ] prA [ = ⊥-elim $ Cover.¬⊙diffʳ prA prS

        open Interleaving

        ⟦>>=⟧ : {σ : ty} {S T U : Usage σ} (Γ₁ Δ₁ Γ₂ Δ₂ : Con ty) {a b : ty}
               (V₁ : Usage σ) (d₁ : T ≡ S ─ V₁) (tm₁ : Γ₁ ++ ｢ V₁ ｣ ++ Δ₁ ⊢ a)
               (V₂ : Usage σ) (d₂ : U ≡ T ─ V₂) (tm₂ : Γ₂ ++ ｢ V₂ ｣ ++ Δ₂ ⊢ b) →
               Σ[ V ∈ Usage σ ] Σ[ S₁ ∈ Con ty ] Σ[ S₂ ∈ Con ty ]
                 U ≡ S ─ V × ｢ V ｣ ≡ S₁ ⋈ S₂
               × Γ₁ ++ S₁ ++ Δ₁ ⊢ a × Γ₂ ++ S₂ ++ Δ₂ ⊢ b
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ V₁ d₁   tm₁ ._ `idˡ tm₂ = V₁ , ｢ V₁ ｣ , ε , d₁   , Interleaving.reflˡ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ `idˡ tm₁ V₂ d₂   tm₂ = V₂ , ε , ｢ V₂ ｣ , d₂   , Interleaving.reflʳ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ `idʳ tm₁ V₂ `idʳ tm₂ = V₂ , ε , ｢ V₂ ｣ , `idʳ , Interleaving.reflʳ , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ] V₁ [ `idʳ tm₁ ] V₂ [ ] pr [ tm₂ =
           _ , Cover.｢ V₁ ｣ , Cover.｢ V₂ ｣ , `idʳ , Cover.｢─｣ pr , tm₁ , tm₂
        ⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ ._ ] prS [ tm₁ ._ ] prT [ tm₂ =
           let (S , S₁ , S₂ , d , jtms) = Cover.⟦>>=⟧ Γ₁ Δ₁ Γ₂ Δ₂ _ prS tm₁ _ prT tm₂
           in ] S [ , S₁ , S₂ , ] d [ , jtms

    module Context where

      open Con
      open Context
      open IMLL.Type Pr
      open IMLL Pr
      open IMLL.RewriteRules Pr
      open Pointwise
      open Context.Context
      open Consumption.Context Pr
      open Action.Context Pr
      open Linearity Pr
      open Linearity.Context Pr

      ⟦⊙⟧ : {γ : Con ty} (δ : Con ty) (Γ : Usage γ) {σ τ : ty} (Δ₁ Δ₂ : Usage γ)
          (E₁ : Usage γ) (d₁ : Δ₁ ≡ Γ ─ E₁) (tm₁ : ｢ E₁ ｣ ++ δ ⊢ σ)
          (E₂ : Usage γ) (d₂ : Δ₂ ≡ Γ ─ E₂) (tm₂ : ｢ E₂ ｣ ++ δ ⊢ τ)
          {Δ : Usage γ} → Δ  ≡ Δ₁ ⊙ Δ₂ →
          Σ[ E ∈ Usage γ ] Δ  ≡ Γ ─ E × ｢ E ｣ ++ δ ⊢ σ × ｢ E ｣ ++ δ ⊢ τ
      ⟦⊙⟧ δ ε ε ε ε d₁ tm₁ ε d₂ tm₂ ε = ε , ε , tm₁ , tm₂
      ⟦⊙⟧ {γ ∙ a} δ (Γ ∙ S) (Δ₁ ∙ D₁) (Δ₂ ∙ D₂)
        (E₁ ∙ e₁) (d₁ ∙ t₁) tm₁ (E₂ ∙ e₂) (d₂ ∙ t₂) tm₂ (sync ∙ prS) =
        let (f , df , tmσ , tmτ) =
              Type.Usage.⟦⊙⟧ ｢ E₁ ｣ ｢ E₂ ｣ δ e₁ t₁ tm₁ e₂ t₂ tm₂ prS
            (E , dE , tmσ , tmτ)  =
              ⟦⊙⟧ (LTU.｢ f ｣ ++ δ) Γ Δ₁ Δ₂
                E₁ d₁ (tm-assoc ｢ E₁ ｣ LTU.｢ f ｣ δ tmσ)
                E₂ d₂ (tm-assoc ｢ E₂ ｣ LTU.｢ f ｣ δ tmτ) sync
        in E ∙ f , dE ∙ df , tm-assoc⁻¹ ｢ E ｣ LTU.｢ f ｣ δ tmσ
                           , tm-assoc⁻¹ ｢ E ｣ LTU.｢ f ｣ δ tmτ

      ⟦&ʳ⟧ : {γ : Con ty} {Γ : Usage γ} {σ τ : ty} {Δ₁ Δ₂ : Usage γ} →
            Σ[ E ∈ Usage γ ] Δ₁ ≡ Γ ─ E × ｢ E ｣ ⊢ σ → 
            Σ[ E ∈ Usage γ ] Δ₂ ≡ Γ ─ E × ｢ E ｣ ⊢ τ →
            (Δ : Usage γ) → Δ  ≡ Δ₁ ⊙ Δ₂ →
            Σ[ E ∈ Usage γ ] Δ  ≡ Γ ─ E × ｢ E ｣ ⊢ σ × ｢ E ｣ ⊢ τ
      ⟦&ʳ⟧ (E₁ , d₁ , tm₁) (E₂ , d₂ , tm₂) Δ = ⟦⊙⟧ ε _ _ _ E₁ d₁ tm₁ E₂ d₂ tm₂

      open Interleaving
      open Interleaving.RewriteRules

      ⟦>>=⟧ : (γ : Con ty) {Γ Δ E : Usage γ} (C A B : Con ty)
             {σ τ : ty} (pr : C ≡ A ⋈ B)
             (F₁ : Usage γ) (d₁ : Δ ≡ Γ ─ F₁) (tm₁ : ｢ F₁ ｣ ++ A ⊢ σ)
             (F₂ : Usage γ) (d₂ : E ≡ Δ ─ F₂) (tm₂ : ｢ F₂ ｣ ++ B ⊢ τ) →
             Σ[ F ∈ Usage γ ] Σ[ E₁ ∈ Con ty ] Σ[ E₂ ∈ Con ty ]
               E ≡ Γ ─ F × ｢ F ｣ ++ C ≡ E₁ ++ A ⋈ E₂ ++ B
             × E₁ ++ A ⊢ σ × E₂ ++ B ⊢ τ
      ⟦>>=⟧ ε C A B pr ε ε h₁ ε ε h₂ = ε , ε , ε , ε , ε Interleaving.++ pr , h₁ , h₂
      ⟦>>=⟧ (γ ∙ σ) C A B pr (F₁ ∙ V₁) (D₁ ∙ d₁) tm₁ (F₂ ∙ V₂) (D₂ ∙ d₂) tm₂ =
        let (V , V₁ , V₂ , d , j , tm₁ , tm₂) =
              Type.Usage.⟦>>=⟧ ｢ F₁ ｣ A ｢ F₂ ｣ B V₁ d₁ tm₁ V₂ d₂ tm₂
            (F , F₁ , F₂ , D , J , tm₁ , tm₂) =
              ⟦>>=⟧ γ (LTU.｢ V ｣ ++ C) (V₁ ++ A) (V₂ ++ B) (j Interleaving.++ pr)
                   F₁ D₁ (tm-assoc ｢ F₁ ｣ V₁ A tm₁)
                   F₂ D₂ (tm-assoc ｢ F₂ ｣ V₂ B tm₂)
        in F ∙ V , F₁ ++ V₁ , F₂ ++ V₂ , D ∙ d
         , ⋈-assoc⁻¹ ｢ F ｣ C F₁ A F₂ B J
         , tm-assoc⁻¹ F₁ V₁ A tm₁
         , tm-assoc⁻¹ F₂ V₂ B tm₂

      ⟦⊗ʳ⟧ : {γ : Con ty} {Γ Δ E : Usage γ} {σ τ : ty} →
            Σ[ F ∈ Usage γ ] Δ ≡ Γ ─ F × ｢ F ｣ ⊢ σ → 
            Σ[ F ∈ Usage γ ] E ≡ Δ ─ F × ｢ F ｣ ⊢ τ →
            Σ[ F ∈ Usage γ ] Σ[ E₁ ∈ Con ty ] Σ[ E₂ ∈ Con ty ]
               E ≡ Γ ─ F × ｢ F ｣ ≡ E₁ ⋈ E₂ × E₁ ⊢ σ × E₂ ⊢ τ
      ⟦⊗ʳ⟧ (F₁ , d₁ , tm₁) (F₂ , d₂ , tm₂) = ⟦>>=⟧ _ ε ε ε ε F₁ d₁ tm₁ F₂ d₂ tm₂

      open Calculus

      ⟦_⟧ : {γ : Con ty} {Γ : Usage γ} {σ : ty} {Δ : Usage γ} (pr : Γ ⊢ σ ⊣ Δ) →
            Σ[ E ∈ Usage γ ] Δ ≡ Γ ─ E × ｢ E ｣ ⊢ σ
      ⟦ `κ pr              ⟧ = BTC.Soundness.⟦ pr ⟧
      ⟦ prσ `⊗ʳ prτ        ⟧ =
        let (F , E₁ , E₂ , diff , inter , tmσ , tmτ) = ⟦⊗ʳ⟧ ⟦ prσ ⟧ ⟦ prτ ⟧
        in F , diff , tmσ `⊗ʳ tmτ by inter
      ⟦ prσ `&ʳ prτ by acc ⟧ =
        let (E , diff , tmσ , tmτ) = ⟦&ʳ⟧ ⟦ prσ ⟧ ⟦ prτ ⟧ _ acc
        in E , diff , tmσ `&ʳ tmτ