module CoercionExpr.CatchUpBack where

open import Data.Nat
open import Data.Unit using (⊀; tt)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.List hiding ([_])
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_)
open import Data.Maybe
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≑_; refl)
open import Function using (case_of_)

open import Common.Utils
open import Common.SecurityLabels
open import Common.BlameLabels
open import CoercionExpr.CoercionExpr
open import CoercionExpr.Precision

data InSync : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²} (c̅₁ : CExpr g₁ β‡’ gβ‚‚) (cΜ…β‚‚ : CExpr g₁′ β‡’ gβ‚‚β€²) β†’ Set where
  v-v : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²} {c̅₁ : CExpr g₁ β‡’ gβ‚‚} {cΜ…β‚‚ : CExpr g₁′ β‡’ gβ‚‚β€²}
    β†’ CVal cΜ…β‚‚
    β†’ ⊒ c̅₁ βŠ‘ cΜ…β‚‚
    β†’ InSync c̅₁ cΜ…β‚‚

  v-βŠ₯ : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²} {c̅₁ : CExpr g₁ β‡’ gβ‚‚} {p}
    β†’ ⊒ c̅₁ βŠ‘ βŠ₯ g₁′ gβ‚‚β€² p
    β†’ InSync c̅₁ (βŠ₯ g₁′ gβ‚‚β€² p)

catchup-back : βˆ€ {β„“ β„“β€² g gβ€²} (cΜ… : CExpr l β„“ β‡’ g) (c̅₁′ : CExpr l β„“β€² β‡’ gβ€²)
  β†’ CVal cΜ…
  β†’ ⊒ cΜ… βŠ‘ c̅₁′
  β†’ βˆƒ[ cΜ…β‚‚β€² ] (c̅₁′ β€”β†  cΜ…β‚‚β€²) Γ— (InSync cΜ… cΜ…β‚‚β€²)
catchup-back (id (l β„“)) (id (l β„“β€²)) id (βŠ‘-id lβŠ‘l) = ⟨ _ , _ ∎ , v-v id (βŠ‘-id lβŠ‘l) ⟩
catchup-back (id (l β„“)) (cΜ…β€² β¨Ύ id β„“β€²) id (βŠ‘-castr x lβŠ‘l lβŠ‘l)
  with catchup-back _ _ id x
... | ⟨ cΜ…β‚™β€² , cΜ…β€²β† cΜ…β‚™β€² , v-v v y ⟩ =
  ⟨ cΜ…β‚™β€² , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚™β€²) (cΜ…β‚™β€² β¨Ύ id (l β„“) β€”β†’βŸ¨ id v ⟩ cΜ…β‚™β€² ∎) , v-v v y ⟩
... | ⟨ βŠ₯ _ _ p , cΜ…β€²β† βŠ₯ , v-βŠ₯ y ⟩ =
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β€²β† βŠ₯) (βŠ₯ _ _ p β¨Ύ id (l β„“) β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ βŠ₯ _ _ p ∎) ,
    v-βŠ₯ y ⟩
catchup-back (id (l β„“)) (βŠ₯ (l _) _ p) id (βŠ‘-βŠ₯ lβŠ‘l lβŠ‘l) =
  ⟨ _ , _ ∎ , v-βŠ₯ (βŠ‘-βŠ₯ lβŠ‘l lβŠ‘l) ⟩

catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ id (l β„“)) (inj v) (βŠ‘-cast cΜ…βŠ‘cΜ…β€² lβŠ‘l β‹†βŠ‘)
  with catchup-back _ _ v cΜ…βŠ‘cΜ…β€²
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-v v x ⟩ =
  ⟨ cΜ…β‚‚β€² , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (cΜ…β‚‚β€² β¨Ύ id (l β„“) β€”β†’βŸ¨ id v ⟩ cΜ…β‚‚β€² ∎) , v-v v (βŠ‘-castl x lβŠ‘l β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ x ⟩
  with precβ†’βŠ‘ _ _ cΜ…βŠ‘cΜ…β€²
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩
catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ β„“ !) (inj v) (βŠ‘-cast cΜ…βŠ‘cΜ…β€² lβŠ‘l β‹†βŠ‘)
  with catchup-back _ _ v cΜ…βŠ‘cΜ…β€²
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-v v x ⟩ =
  ⟨ cΜ…β‚‚β€² β¨Ύ β„“ ! , plug-cong cΜ…β€²β† cΜ…β‚‚β€² , v-v (inj v) (βŠ‘-cast x lβŠ‘l β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ x ⟩
  with precβ†’βŠ‘ _ _ cΜ…βŠ‘cΜ…β€²
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩
catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ ↑) (inj v) (βŠ‘-cast cΜ…βŠ‘cΜ…β€² lβŠ‘l β‹†βŠ‘)
  with catchup-back _ _ v cΜ…βŠ‘cΜ…β€²
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-v v x ⟩ =
  ⟨ cΜ…β‚‚β€² β¨Ύ ↑ , plug-cong cΜ…β€²β† cΜ…β‚‚β€² , v-v (up v) (βŠ‘-cast x lβŠ‘l β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ x ⟩
  with precβ†’βŠ‘ _ _ cΜ…βŠ‘cΜ…β€²
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩

catchup-back (cΜ… β¨Ύ β„“ !) c̅₁′ (inj v) (βŠ‘-castl x lβŠ‘l β‹†βŠ‘)
  with catchup-back cΜ… c̅₁′ v x
... | ⟨ cΜ…β‚‚β€² , c̅₁′↠cΜ…β‚‚β€² , v-v v y ⟩ =
  ⟨ cΜ…β‚‚β€² , c̅₁′↠cΜ…β‚‚β€² , v-v v (βŠ‘-castl y lβŠ‘l β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚‚β€² , c̅₁′↠βŠ₯ , v-βŠ₯ y ⟩ =
  ⟨ βŠ₯ _ _ _ , c̅₁′↠βŠ₯ , v-βŠ₯ (βŠ‘-castl y lβŠ‘l β‹†βŠ‘) ⟩

catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ id gβ€²) (inj v) (βŠ‘-castr x β‹†βŠ‘ β‹†βŠ‘)
  with catchup-back (cΜ… β¨Ύ β„“ !) cΜ…β€² (inj v) x
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-v v y ⟩ =
  ⟨ cΜ…β‚‚β€² , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (cΜ…β‚‚β€² β¨Ύ id gβ€² β€”β†’βŸ¨ id v ⟩ cΜ…β‚‚β€² ∎) , v-v v y ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ y ⟩
  with precβ†’βŠ‘ _ _ y
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩
catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ ↑) (inj v) (βŠ‘-castr x β‹†βŠ‘ β‹†βŠ‘)
  with catchup-back (cΜ… β¨Ύ β„“ !) cΜ…β€² (inj v) x
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-v v y ⟩ =
  ⟨ cΜ…β‚‚β€² β¨Ύ ↑ , plug-cong cΜ…β€²β† cΜ…β‚‚β€² , v-v (up v) (βŠ‘-castr y β‹†βŠ‘ β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ y ⟩
  with precβ†’βŠ‘ _ _ y
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩
catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ β„“β€² !) (inj v) (βŠ‘-castr x β‹†βŠ‘ β‹†βŠ‘)
  with catchup-back (cΜ… β¨Ύ β„“ !) cΜ…β€² (inj v) x
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-v v y ⟩ =
  ⟨ cΜ…β‚‚β€² β¨Ύ β„“β€² ! , plug-cong cΜ…β€²β† cΜ…β‚‚β€² , v-v (inj v) (βŠ‘-castr y β‹†βŠ‘ β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ y ⟩
  with precβ†’βŠ‘ _ _ y
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩
catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ low ?? p) (inj v) (βŠ‘-castr x β‹†βŠ‘ β‹†βŠ‘)
  with catchup-back (cΜ… β¨Ύ β„“ !) cΜ…β€² (inj v) x
... | ⟨ cΜ…β‚™β€² β¨Ύ low ! , cΜ…β€²β† cΜ…β‚‚β€² , v-v (inj vβ€²) y ⟩ =
  ⟨ cΜ…β‚™β€² , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (cΜ…β‚™β€² β¨Ύ (low !) β¨Ύ (low ?? p) β€”β†’βŸ¨ ?-id vβ€² ⟩ cΜ…β‚™β€² ∎) ,
    v-v vβ€² (prec-inj-left _ _ (inj v) vβ€² y) ⟩
... | ⟨ cΜ…β‚™β€² β¨Ύ high ! , cΜ…β€²β† cΜ…β‚‚β€² , v-v (inj vβ€²) y ⟩ =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ y in
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (cΜ…β‚™β€² β¨Ύ (high !) β¨Ύ (low ?? p) β€”β†’βŸ¨ ?-βŠ₯ vβ€² ⟩ βŠ₯ _ (l low) p ∎) ,
    v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ y ⟩
  with precβ†’βŠ‘ _ _ y
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩
catchup-back (cΜ… β¨Ύ β„“ !) (cΜ…β€² β¨Ύ high ?? p) (inj v) (βŠ‘-castr x β‹†βŠ‘ β‹†βŠ‘)
  with catchup-back (cΜ… β¨Ύ β„“ !) cΜ…β€² (inj v) x
... | ⟨ cΜ…β‚™β€² β¨Ύ low ! , cΜ…β€²β† cΜ…β‚‚β€² , v-v (inj vβ€²) y ⟩ =
  ⟨ cΜ…β‚™β€² β¨Ύ ↑ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (cΜ…β‚™β€² β¨Ύ (low !) β¨Ύ (high ?? p) β€”β†’βŸ¨ ?-↑ vβ€² ⟩ cΜ…β‚™β€² β¨Ύ ↑ ∎) ,
    v-v (up vβ€²) (βŠ‘-castr (prec-inj-left _ _ (inj v) vβ€² y) β‹†βŠ‘ β‹†βŠ‘) ⟩
... | ⟨ cΜ…β‚™β€² β¨Ύ high ! , cΜ…β€²β† cΜ…β‚‚β€² , v-v (inj vβ€²) y ⟩ =
  ⟨ cΜ…β‚™β€² , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (cΜ…β‚™β€² β¨Ύ (high !) β¨Ύ (high ?? p) β€”β†’βŸ¨ ?-id vβ€² ⟩ cΜ…β‚™β€² ∎) ,
    v-v vβ€² (prec-inj-left _ _ (inj v) vβ€² y) ⟩
... | ⟨ cΜ…β‚‚β€² , cΜ…β€²β† cΜ…β‚‚β€² , v-βŠ₯ y ⟩
  with precβ†’βŠ‘ _ _ y
... | ⟨ β„“βŠ‘β„“β€² , _ ⟩ =
  ⟨ βŠ₯ _ _ _ , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚‚β€²) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² β‹†βŠ‘) ⟩

catchup-back (cΜ… β¨Ύ β„“ !) (βŠ₯ (l _) _ p) (inj v) (βŠ‘-βŠ₯ lβŠ‘l β‹†βŠ‘) = ⟨ _ , _ ∎ , v-βŠ₯ (βŠ‘-βŠ₯ lβŠ‘l β‹†βŠ‘) ⟩
catchup-back (cΜ… β¨Ύ ↑) (cΜ…β€² β¨Ύ ↑) (up v) (βŠ‘-cast x lβŠ‘l lβŠ‘l)
  with catchup-back cΜ… cΜ…β€² v x
... | ⟨ cΜ…β‚™β€² , cΜ…β€²β† cΜ…β‚™β€² , v-v v y ⟩ =
  ⟨ cΜ…β‚™β€² β¨Ύ ↑ , plug-cong cΜ…β€²β† cΜ…β‚™β€² , v-v (up v) (βŠ‘-cast y lβŠ‘l lβŠ‘l) ⟩
... | ⟨ βŠ₯ _ _ p , cΜ…β€²β† βŠ₯ , v-βŠ₯ y ⟩ =
  let ⟨ β„“βŠ‘β„“β€² , _ ⟩ = precβ†’βŠ‘ _ _ x in
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β€²β† βŠ₯) (βŠ₯ _ _ p β¨Ύ ↑ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ βŠ₯ _ _ p ∎) ,
    v-βŠ₯ (βŠ‘-βŠ₯ β„“βŠ‘β„“β€² lβŠ‘l) ⟩
catchup-back (cΜ… β¨Ύ ↑) (cΜ…β€² β¨Ύ id _) (up v) (βŠ‘-cast x lβŠ‘l ())
catchup-back (cΜ… β¨Ύ ↑) c̅₁′ (up v) (βŠ‘-castl x lβŠ‘l ())
catchup-back (cΜ… β¨Ύ ↑) (cΜ…β€² β¨Ύ id (l high)) (up v) (βŠ‘-castr x lβŠ‘l lβŠ‘l)
  with catchup-back (cΜ… β¨Ύ ↑) cΜ…β€² (up v) x
... | ⟨ cΜ…β‚™β€² , cΜ…β€²β† cΜ…β‚™β€² , v-v v y ⟩ =
  ⟨ cΜ…β‚™β€² , β† -trans (plug-cong cΜ…β€²β† cΜ…β‚™β€²) (cΜ…β‚™β€² β¨Ύ id (l high) β€”β†’βŸ¨ id v ⟩ cΜ…β‚™β€² ∎) , v-v v y ⟩
... | ⟨ βŠ₯ _ _ p , cΜ…β€²β† βŠ₯ , v-βŠ₯ y ⟩ =
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β€²β† βŠ₯) (βŠ₯ _ _ p β¨Ύ id (l high) β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ βŠ₯ _ _ p ∎) ,
    v-βŠ₯ y ⟩
catchup-back (cΜ… β¨Ύ ↑) (βŠ₯ (l _) _ p) (up v) (βŠ‘-βŠ₯ lβŠ‘l lβŠ‘l) =
  ⟨ βŠ₯ _ _ p , _ ∎ , v-βŠ₯ (βŠ‘-βŠ₯ lβŠ‘l lβŠ‘l) ⟩


catchup-back-right : βˆ€ {g β„“β€² gβ€²} (c̅₁′ : CExpr l β„“β€² β‡’ gβ€²)
  β†’ ⊒ id g βŠ‘ c̅₁′
  β†’ βˆƒ[ cΜ…β‚‚β€² ] (c̅₁′ β€”β†  cΜ…β‚‚β€²) Γ— (InSync (id g) cΜ…β‚‚β€²)
catchup-back-right {l β„“} c̅₁′ prec = catchup-back (id (l β„“)) c̅₁′ id prec
catchup-back-right {⋆} (id (l β„“β€²)) (βŠ‘-id β‹†βŠ‘) =
  ⟨ _ , _ ∎ , v-v id (βŠ‘-id β‹†βŠ‘) ⟩
catchup-back-right {⋆} (cΜ…β€² β¨Ύ cβ€²) (βŠ‘-castr idβ‹†βŠ‘cΜ…β€² β‹†βŠ‘ β‹†βŠ‘)
  with catchup-back-right _ idβ‹†βŠ‘cΜ…β€²
... | ⟨ βŠ₯ _ _ p , cΜ…β€²β† βŠ₯ , v-βŠ₯ (βŠ‘-βŠ₯ β‹†βŠ‘ β‹†βŠ‘) ⟩ =
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β€²β† βŠ₯) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎) , v-βŠ₯ (βŠ‘-βŠ₯ β‹†βŠ‘ β‹†βŠ‘) ⟩
... | ⟨ cΜ…β€³ , cΜ…β€²β† cΜ…β€³ , v-v 𝓋″ idβ‹†βŠ‘cΜ…β€³ ⟩ with cβ€²
... | id gβ€² =
  ⟨ cΜ…β€³ , β† -trans (plug-cong cΜ…β€²β† cΜ…β€³) (cΜ…β€³ β¨Ύ id gβ€² β€”β†’βŸ¨ id 𝓋″ ⟩ cΜ…β€³ ∎) , v-v 𝓋″ idβ‹†βŠ‘cΜ…β€³ ⟩
... | ↑ =
  ⟨ cΜ…β€³ β¨Ύ ↑ , plug-cong cΜ…β€²β† cΜ…β€³ , v-v (up 𝓋″) (βŠ‘-castr idβ‹†βŠ‘cΜ…β€³ β‹†βŠ‘ β‹†βŠ‘) ⟩
... | β„“β€² ! =
  ⟨ cΜ…β€³ β¨Ύ β„“β€² ! , plug-cong cΜ…β€²β† cΜ…β€³ , v-v (inj 𝓋″) (βŠ‘-castr idβ‹†βŠ‘cΜ…β€³ β‹†βŠ‘ β‹†βŠ‘) ⟩
... | β„“β€² ?? p with 𝓋″ | β„“β€²
...   | (inj (id {l low})) | low =
  ⟨ id (l low) , β† -trans (plug-cong cΜ…β€²β† cΜ…β€³) (_ β€”β†’βŸ¨ ?-id id ⟩ _ ∎) ,
    v-v id (βŠ‘-id β‹†βŠ‘) ⟩
...   | (inj (id {l high})) | low =
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β€²β† cΜ…β€³) (_ β€”β†’βŸ¨ ?-βŠ₯ id ⟩ _ ∎) ,
    v-βŠ₯ (βŠ‘-βŠ₯ β‹†βŠ‘ β‹†βŠ‘) ⟩
...   | (inj (id {l low})) | high =
  ⟨ id (l low) β¨Ύ ↑ , β† -trans (plug-cong cΜ…β€²β† cΜ…β€³) (_ β€”β†’βŸ¨ ?-↑ id ⟩ _ ∎) ,
    v-v (up id) (βŠ‘-castr (βŠ‘-id β‹†βŠ‘) β‹†βŠ‘ β‹†βŠ‘) ⟩
...   | (inj (id {l high})) | high =
  ⟨ id (l high) , β† -trans (plug-cong cΜ…β€²β† cΜ…β€³) (_ β€”β†’βŸ¨ ?-id id ⟩ _ ∎) ,
    v-v id (βŠ‘-id β‹†βŠ‘) ⟩
...   | (inj (up id)) | low =
  ⟨ βŠ₯ _ _ p , β† -trans (plug-cong cΜ…β€²β† cΜ…β€³) (_ β€”β†’βŸ¨ ?-βŠ₯ (up id) ⟩ _ ∎) ,
    v-βŠ₯ (βŠ‘-βŠ₯ β‹†βŠ‘ β‹†βŠ‘) ⟩
...   | (inj (up id)) | high =
  ⟨ id (l low) β¨Ύ ↑ , β† -trans (plug-cong cΜ…β€²β† cΜ…β€³) (_ β€”β†’βŸ¨ ?-id (up id) ⟩ _ ∎) ,
    v-v (up id) (βŠ‘-castr (βŠ‘-id β‹†βŠ‘) β‹†βŠ‘ β‹†βŠ‘) ⟩
catchup-back-right {⋆} (βŠ₯ (l _) _ p) (βŠ‘-βŠ₯ β‹†βŠ‘ β‹†βŠ‘) =
  ⟨ βŠ₯ _ _ p , _ ∎ , v-βŠ₯ (βŠ‘-βŠ₯ β‹†βŠ‘ β‹†βŠ‘) ⟩