PLT-7103 Adapt Scoped Renaming/Substitution and Extrication to SOPs i…

…n the metatheory (#5597)

* PLT-7103 Adapt Erasure, Scoped, Extrication to SOPs

plutus-metatheory/src/Algorithmic/Erasure.lagda

@@ -194,6 +194,10 @@ lem-erase' {Γ = Γ} p t = trans
   (sym (lem-subst (erase t) (lem≡Ctx {Γ = Γ} refl)))
   (lem-erase refl p t)
 
+lem-erase'' : ∀{Φ Γ}{A A' : Φ ⊢Nf⋆ *}(q : A ≡ A')(t : Γ A.⊢ A)
+  → erase t  ≡ erase (subst (Γ A.⊢_) q t)
+lem-erase'' refl t = refl  
+
 same : ∀{Φ Γ}{A : Φ ⊢⋆ *}(t : Γ D.⊢ A)
   → D.erase t ≡ subst _⊢ (lenLemma Γ) (erase (nfType t)) 
 

plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda

@@ -3,26 +3,30 @@ module Algorithmic.Erasure.RenamingSubstitution where
 \end{code}
 
 \begin{code}
-open import Relation.Binary.PropositionalEquality using (_≡_;refl;sym;trans;cong;cong₂)
+open import Relation.Binary.PropositionalEquality using (_≡_;refl;sym;trans;subst;cong;cong₂)
 open import Function using (id;_∘_)
+open import Data.Vec using (Vec;_∷_;lookup)
+open import Data.Fin using (Fin;toℕ)
 
 open import Utils using (Kind;*;Maybe;nothing;just)
+open import Utils.List using (List;[];_∷_)
 open import Type using (Ctx⋆;∅;_,⋆_;_∋⋆_;Z;S)
 import Type.RenamingSubstitution as ⋆
-open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;weakenNf;renNf)
+open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;weakenNf;renNf;lookup-renNf-VecList;embNf;embNf-VecList;lookup-embNf-VecList)
 open _⊢Nf⋆_
 open _⊢Ne⋆_
+open import Type.BetaNBE using (lookup-eval-VecList;idEnv)
 open import Type.BetaNormal.Equality using (renNf-id;renNf-comp)
 open import Type.BetaNBE.RenamingSubstitution 
                 using (ren[]Nf;ren-nf-μ;SubNf;subNf-id;subNf;weakenNf[];weakenNf-subNf)
                 using (sub-nf-Π;sub[]Nf';sub-nf-μ;subNf-cons;extsNf)
-open import Algorithmic as A using (Ctx;_∋_;conv∋;_⊢_;conv⊢)
+open import Algorithmic as A using (Ctx;_∋_;conv∋;_⊢_;conv⊢;Cases;[];_∷_)
 open import Algorithmic.Signature using (btype-ren;btype-sub)
 open Ctx
 open _∋_
 open _⊢_
 import Algorithmic.RenamingSubstitution as A
-open import Algorithmic.Erasure using (len;erase;eraseTC;eraseVar;lem-erase)
+open import Algorithmic.Erasure using (len;erase;eraseTC;eraseVar;lem-erase;erase-Cases;erase-ConstrArgs;lem-erase'')
 open import Untyped using (_⊢)
 open _⊢
 import Untyped.RenamingSubstitution as U
@@ -117,6 +121,36 @@ ext⋆-erase {Γ = Γ} ρ⋆ ρ α = conv∋-erase
 ren-erase : ∀{Φ Ψ}{Γ : Ctx Φ}{Δ : Ctx Ψ}(ρ⋆ : ⋆.Ren Φ Ψ)
   → (ρ : A.Ren ρ⋆ Γ Δ){A : Φ ⊢Nf⋆ *} → (t : Γ ⊢ A)
   →  erase (A.ren ρ⋆ ρ t) ≡ U.ren (erase-Ren ρ⋆ ρ) (erase t)
+
+ren-erase-ConstrArgs-List : ∀ {Φ} {Ψ} {Γ : Ctx Φ} {Δ : Ctx Ψ}
+                              (ρ⋆ : ⋆.Ren Φ Ψ) (ρ : A.Ren ρ⋆ Γ Δ)
+                              {As : List (Φ ⊢Nf⋆ *)}
+                              (cs : A.ConstrArgs Γ As) →
+                            erase-ConstrArgs ((A.ren-ConstrArgs-List ρ⋆ ρ cs)) ≡
+                            U.renList (erase-Ren ρ⋆ ρ) (erase-ConstrArgs cs)
+ren-erase-ConstrArgs-List ρ⋆ ρ [] = refl
+ren-erase-ConstrArgs-List ρ⋆ ρ (x ∷ cs) = cong₂ _∷_ (ren-erase ρ⋆ ρ x) (ren-erase-ConstrArgs-List ρ⋆ ρ cs)
+
+ren-erase-ConstrArgs : ∀ {Φ} {Ψ} {Γ : Ctx Φ} {Δ : Ctx Ψ}
+                         (ρ⋆ : ⋆.Ren Φ Ψ) (ρ : A.Ren ρ⋆ Γ Δ) {n} (i : Fin n)
+                         (Tss : Vec (List (Φ ⊢Nf⋆ *)) n)
+                         (cs : A.ConstrArgs Γ (lookup Tss i)) →
+                       erase-ConstrArgs (A.ren-ConstrArgs ρ⋆ ρ i Tss cs)
+                       ≡ U.renList (erase-Ren ρ⋆ ρ)(erase-ConstrArgs cs)
+ren-erase-ConstrArgs ρ⋆ ρ i Tss cs rewrite lookup-renNf-VecList ρ⋆ i Tss = ren-erase-ConstrArgs-List ρ⋆ ρ cs                 
+
+ren-erase-Cases : ∀{Φ Ψ}{Γ : Ctx Φ}{Δ : Ctx Ψ}
+  → (ρ⋆ : ⋆.Ren Φ Ψ)
+  → (ρ : A.Ren ρ⋆ Γ Δ)
+  → ∀ {n}{A : Φ ⊢Nf⋆ *}{Tss : Vec (List (Φ ⊢Nf⋆ *)) n}
+  → (cs : Cases Γ A Tss)
+  →  erase-Cases (A.ren-Cases ρ⋆ ρ cs) ≡ U.renList (erase-Ren ρ⋆ ρ) (erase-Cases cs)
+ren-erase-Cases ρ⋆ ρ [] = refl
+ren-erase-Cases ρ⋆ ρ {Tss = As ∷ _}(c ∷ cs) = 
+      cong₂ _∷_ (trans (sym (lem-erase'' (A.ren-mkCaseType ρ⋆ As) (A.ren ρ⋆ ρ c)))
+                       (ren-erase ρ⋆ ρ c)) 
+                (ren-erase-Cases ρ⋆ ρ cs)
+
 ren-erase ρ⋆ ρ (` x) = cong
   `
   (cong-erase-ren
@@ -146,8 +180,10 @@ ren-erase ρ⋆ ρ (unwrap {A = A}{B = B} t refl) = trans
   (conv⊢-erase (sym (ren-nf-μ ρ⋆ A B)) (unwrap (A.ren ρ⋆ ρ t) refl))
   (ren-erase ρ⋆ ρ t)
 ren-erase ρ⋆ ρ (con c refl)            = refl
-ren-erase ρ⋆ ρ (builtin b / refl)        =
- sym (lem-erase refl (btype-ren b ρ⋆) (builtin b / refl))
+ren-erase ρ⋆ ρ (builtin b / refl)      =
+  sym (lem-erase refl (btype-ren b ρ⋆) (builtin b / refl))
+ren-erase ρ⋆ ρ (constr i A refl cs) = cong (constr (toℕ i)) (ren-erase-ConstrArgs ρ⋆ ρ i A cs)
+ren-erase ρ⋆ ρ (case t cases) = cong₂ case (ren-erase ρ⋆ ρ t) (ren-erase-Cases ρ⋆ ρ cases)
 ren-erase ρ⋆ ρ (error A)          = refl
 --
 erase-Sub : ∀{Φ Ψ}{Γ : Ctx Φ}{Δ : Ctx Ψ}(σ⋆ : SubNf Φ Ψ)
@@ -192,7 +228,39 @@ exts⋆-erase {Γ = Γ}{Δ} σ⋆ σ {B} α = trans
 
 sub-erase : ∀{Φ Ψ}{Γ : Ctx Φ}{Δ : Ctx Ψ}(σ⋆ : SubNf Φ Ψ)
   → (σ : A.Sub σ⋆ Γ Δ){A : Φ ⊢Nf⋆ *} → (t : Γ ⊢ A)
-  →  erase (A.sub σ⋆ σ t) ≡ U.sub (erase-Sub σ⋆ σ) (erase t) 
+  →  erase (A.sub σ⋆ σ t) ≡ U.sub (erase-Sub σ⋆ σ) (erase t)
+
+
+sub-Erase-ConstrList : ∀ {Φ}{Ψ}{Γ : Ctx Φ} {Δ : Ctx Ψ}
+                         {As : List (Φ ⊢Nf⋆ *)}  
+                         (σ⋆ : SubNf Φ Ψ) (σ : A.Sub σ⋆ Γ Δ)
+                         (cs : A.ConstrArgs Γ As) 
+       →   erase-ConstrArgs (A.sub-ConstrList σ⋆ σ cs) 
+         ≡ U.subList (λ i₁ → erase (σ (backVar Γ i₁))) (erase-ConstrArgs cs)
+sub-Erase-ConstrList σ⋆ σ [] = refl
+sub-Erase-ConstrList σ⋆ σ (x ∷ cs) = cong₂ _∷_ (sub-erase σ⋆ σ x) (sub-Erase-ConstrList σ⋆ σ cs) 
+
+sub-Erase-ConstrArgs : ∀ {Φ} {Ψ} {Γ : Ctx Φ} {Δ : Ctx Ψ}
+                         (σ⋆ : SubNf Φ Ψ) (σ : A.Sub σ⋆ Γ Δ) {n} (i : Fin n)
+                         (Tss : Vec (List (Φ ⊢Nf⋆ *)) n)
+                         (cs : A.ConstrArgs Γ (lookup Tss i)) 
+                → erase-ConstrArgs (A.sub-VecList σ⋆ σ i Tss cs) ≡ U.subList (erase-Sub σ⋆ σ) (erase-ConstrArgs cs)
+sub-Erase-ConstrArgs σ⋆ σ i Tss cs 
+     rewrite lookup-eval-VecList i (⋆.sub-VecList (λ x₁ → embNf (σ⋆ x₁)) (embNf-VecList Tss)) 
+                                   (idEnv _) 
+            | ⋆.lookup-sub-VecList (λ x₁ → embNf (σ⋆ x₁)) i (embNf-VecList Tss)  
+            | lookup-embNf-VecList i Tss = sub-Erase-ConstrList σ⋆ σ cs 
+
+sub-erase-Cases : ∀ {Φ} {Ψ} {Γ : Ctx Φ} {Δ : Ctx Ψ}
+                    (σ⋆ : SubNf Φ Ψ) (σ : A.Sub σ⋆ Γ Δ) {A : Φ ⊢Nf⋆ *} {n}
+                    {Tss : Vec (List (Φ ⊢Nf⋆ *)) n}
+                    (cases : Cases Γ A Tss) →
+                  erase-Cases (A.sub-Cases σ⋆ σ cases) ≡
+                  U.subList (erase-Sub σ⋆ σ) (erase-Cases cases)
+sub-erase-Cases σ⋆ σ [] = refl
+sub-erase-Cases {Δ = Δ} σ⋆ σ {Tss = As ∷ _} (c ∷ cases) = cong₂ _∷_ (trans (sym (lem-erase'' (A.sub-mkCaseType σ⋆ As) (A.sub σ⋆ σ c))) (sub-erase σ⋆ σ c)) 
+                                             (sub-erase-Cases σ⋆ σ cases)
+
 sub-erase σ⋆ σ (` x) =   cong-erase-sub
     σ⋆
     σ
@@ -209,7 +277,9 @@ sub-erase σ⋆ σ (Λ {B = B} t) = cong
   (trans (conv⊢-erase (sub-nf-Π σ⋆ B) (A.sub (extsNf σ⋆) (A.exts⋆ σ⋆ σ) t))
          (trans (sub-erase (extsNf σ⋆) (A.exts⋆ σ⋆ σ) t)
                 (U.sub-cong (exts⋆-erase σ⋆ σ {B = Π B}) (erase t))))
-sub-erase σ⋆ σ (_·⋆_/_ {B = B} t A refl) = trans (conv⊢-erase (sym (sub[]Nf' σ⋆ A B)) (A.sub σ⋆ σ t ·⋆ subNf σ⋆ A / refl)) (cong force (sub-erase σ⋆ σ t))
+sub-erase σ⋆ σ (_·⋆_/_ {B = B} t A refl) = 
+  trans (conv⊢-erase (sym (sub[]Nf' σ⋆ A B)) (A.sub σ⋆ σ t ·⋆ subNf σ⋆ A / refl)) 
+        (cong force (sub-erase σ⋆ σ t))
 sub-erase σ⋆ σ (wrap A B t) = trans
   (conv⊢-erase (sub-nf-μ σ⋆ A B) (A.sub σ⋆ σ t))
   (sub-erase σ⋆ σ t)
@@ -219,6 +289,8 @@ sub-erase σ⋆ σ (unwrap {A = A}{B} t refl) = trans
 sub-erase σ⋆ σ (con c refl) = refl
 sub-erase σ⋆ σ (builtin b / refl) =
  sym (lem-erase refl (btype-sub b σ⋆) (builtin b / refl))
+sub-erase σ⋆ σ (constr i A refl cs) = cong (constr (toℕ i)) (sub-Erase-ConstrArgs σ⋆ σ i A cs)
+sub-erase σ⋆ σ (case t cases) = cong₂ case (sub-erase σ⋆ σ t) (sub-erase-Cases σ⋆ σ cases)
 sub-erase σ⋆ σ (error A) = refl
 
 lem[]⋆ : ∀{Φ}{Γ : Ctx Φ}{K}{B : Φ ,⋆ K ⊢Nf⋆ *}(N : Γ ,⋆ K ⊢ B)(A : Φ ⊢Nf⋆ K)

plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda

@@ -7,24 +7,26 @@ erasure commutes with renaming/substitution
 \begin{code}
 open import Data.Nat using (ℕ)
 open import Data.Fin using (Fin;zero;suc)
+open import Data.Vec using (Vec;[];_∷_)
 open import Data.Product using (Σ;proj₁;proj₂) renaming (_,_ to _,,_)
 open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_;refl;sym;trans;cong;cong₂)
 
 open import Utils using (Kind;*)
+open import Utils.List using (List;[];_∷_)
 open import Type using (Ctx⋆;_,⋆_;_∋⋆_;Z;S)
 open import Algorithmic using (Ctx;_⊢_)
 open Ctx
 import Algorithmic.RenamingSubstitution as As
 import Type.RenamingSubstitution as T
-open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;renNf;renNe)
+open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;renNf;renNe;renNf-VecList;renNf-List)
 open _⊢Nf⋆_
 open _⊢Ne⋆_
 open import Type.BetaNBE.RenamingSubstitution using (extsNf)
 open import Scoped using (ScopedTy)
 open ScopedTy
-open import Scoped.Extrication using (len⋆;extricateVar⋆;extricateNf⋆;extricateNe⋆;extricate)
-open import Scoped.RenamingSubstitution as SS using (Ren⋆;lift⋆;ren⋆;ren⋆-cong;Sub⋆;slift⋆)
+open import Scoped.Extrication using (len⋆;extricateVar⋆;extricateNf⋆;extricateNe⋆;extricate;extricateNf⋆-VecList;extricateNf⋆-List)
+open import Scoped.RenamingSubstitution as SS using (Ren⋆;lift⋆;ren⋆;ren⋆-cong;Sub⋆;slift⋆;ren⋆-List;ren⋆-ListList)
 import Builtin.Constant.Type as AC
 import Builtin.Constant.Type as SC
 
@@ -85,6 +87,20 @@ ren-extricateNe⋆ ρ⋆ (A · B) =
   cong₂ _·_ (ren-extricateNe⋆ ρ⋆ A) (ren-extricateNf⋆ ρ⋆ B)
 ren-extricateNe⋆ ρ⋆ (^ x) = refl
 
+ren-extricateNf⋆-List :  ∀{Γ Δ J}
+  → (ρ⋆ : ∀ {J} → Γ ∋⋆ J → Δ ∋⋆ J)
+  → (xs : List (Γ ⊢Nf⋆ J)) 
+  → ren⋆-List (extricateRenNf⋆ ρ⋆) (extricateNf⋆-List xs) ≡ extricateNf⋆-List (renNf-List ρ⋆ xs)
+ren-extricateNf⋆-List ρ⋆ [] = refl
+ren-extricateNf⋆-List ρ⋆ (x ∷ xs) = cong₂ Utils._∷_ (ren-extricateNf⋆ ρ⋆ x) (ren-extricateNf⋆-List ρ⋆ xs)
+
+ren-extricateNf⋆-ListList :  ∀{Γ Δ J}{n}
+  → (ρ⋆ : ∀ {J} → Γ ∋⋆ J → Δ ∋⋆ J)
+  → (A : Vec (List (Γ ⊢Nf⋆ J)) n)
+  → ren⋆-ListList (extricateRenNf⋆ ρ⋆) (extricateNf⋆-VecList A) ≡ extricateNf⋆-VecList (renNf-VecList ρ⋆ A)
+ren-extricateNf⋆-ListList ρ⋆ [] = refl
+ren-extricateNf⋆-ListList ρ⋆ (xs ∷ xss) = cong₂ Utils._∷_ (ren-extricateNf⋆-List ρ⋆ xs) (ren-extricateNf⋆-ListList ρ⋆ xss)
+
 ren-extricateNf⋆ ρ⋆ (Π A)  =
   cong (Π _)
        (trans (ren⋆-cong (lift⋆-ext ρ⋆) (extricateNf⋆ A))
@@ -98,6 +114,7 @@ ren-extricateNf⋆ ρ⋆ (ne A)   = ren-extricateNe⋆ ρ⋆ A
 ren-extricateNf⋆ ρ⋆ (con (ne x)) =  ren-extricateNe⋆ ρ⋆ x
 ren-extricateNf⋆ ρ⋆ (μ A B)  =
   cong₂ μ (ren-extricateNf⋆ ρ⋆ A) (ren-extricateNf⋆ ρ⋆ B)
+ren-extricateNf⋆ ρ⋆ (SOP xss) = cong SOP (ren-extricateNf⋆-ListList ρ⋆ xss)
 
 extricateSubNf⋆ : ∀{Γ Δ}(σ⋆ : ∀ {J} → Γ ∋⋆ J → Δ ⊢Nf⋆ J) 
   → Sub⋆ (len⋆ Γ) (len⋆ Δ)

plutus-metatheory/src/Scoped/RenamingSubstitution.lagda

@@ -9,6 +9,7 @@ open import Data.Vec using ([];_∷_)
 open import Function using (id)
 open import Relation.Binary.PropositionalEquality using (_≡_;refl;cong;cong₂)
 
+open import Utils using (List;[];_∷_)
 open import Scoped using (ScopedTy;Tel;Tel⋆;Weirdℕ;WeirdFin;ScopedTm)
 open ScopedTy
 open ScopedTm
@@ -27,13 +28,23 @@ lift⋆ ρ zero    = zero
 lift⋆ ρ (suc α) = suc (ρ α)
 
 ren⋆ : ∀{m n} → Ren⋆ m n → ScopedTy m → ScopedTy n
-ren⋆ ρ (` α) = ` (ρ α)
-ren⋆ ρ (A ⇒ B) = ren⋆ ρ A ⇒ ren⋆ ρ B
-ren⋆ ρ (Π K A) = Π K (ren⋆ (lift⋆ ρ) A)
-ren⋆ ρ (ƛ K A) = ƛ K (ren⋆ (lift⋆ ρ) A)
-ren⋆ ρ (A · B) = ren⋆ ρ A · ren⋆ ρ B
-ren⋆ ρ (con c) = con c
-ren⋆ ρ (μ A B) = μ (ren⋆ ρ A) (ren⋆ ρ B)
+
+ren⋆-List : ∀{m n} → Ren⋆ m n → List (ScopedTy m) → List (ScopedTy n)
+ren⋆-List ρ [] = []
+ren⋆-List ρ (x ∷ xs) = (ren⋆ ρ x) ∷ (ren⋆-List ρ xs)
+
+ren⋆-ListList : ∀{m n} → Ren⋆ m n → List (List (ScopedTy m)) → List (List (ScopedTy n))
+ren⋆-ListList ρ [] = []
+ren⋆-ListList ρ (xs ∷ xss) = (ren⋆-List ρ xs) ∷ (ren⋆-ListList ρ xss)
+
+ren⋆ ρ (` α)     = ` (ρ α)
+ren⋆ ρ (A ⇒ B)   = ren⋆ ρ A ⇒ ren⋆ ρ B
+ren⋆ ρ (Π K A)   = Π K (ren⋆ (lift⋆ ρ) A)
+ren⋆ ρ (ƛ K A)   = ƛ K (ren⋆ (lift⋆ ρ) A)
+ren⋆ ρ (A · B)   = ren⋆ ρ A · ren⋆ ρ B
+ren⋆ ρ (con c)   = con c
+ren⋆ ρ (μ A B)   = μ (ren⋆ ρ A) (ren⋆ ρ B)
+ren⋆ ρ (SOP xss) = SOP (ren⋆-ListList ρ xss)
 
 ren⋆T : ∀{m n o} → Ren⋆ m n → Tel⋆ m o → Tel⋆ n o
 ren⋆T ρ⋆ []       = []
@@ -54,6 +65,12 @@ ren : ∀{m n}{w : Weirdℕ m}{v : Weirdℕ n} → Ren⋆ m n → Ren w v → Sc
 renT : ∀{m n o}{w : Weirdℕ m}{v : Weirdℕ n} → Ren⋆ m n → Ren w v
   → Tel w o → Tel v o
 
+ren-List : ∀{m n}{w : Weirdℕ m}{v : Weirdℕ n} → Ren⋆ m n → Ren w v 
+         → List (ScopedTm w)
+         → List (ScopedTm v)
+ren-List ρ⋆ ρ [] = []
+ren-List ρ⋆ ρ (x ∷ xs) = (ren ρ⋆ ρ x) ∷ (ren-List ρ⋆ ρ xs)
+
 ren ρ⋆ ρ (` x) = ` (ρ x)
 ren ρ⋆ ρ (Λ K t) = Λ K (ren (lift⋆ ρ⋆) (⋆lift ρ) t) 
 ren ρ⋆ ρ (t ·⋆ A) = ren ρ⋆ ρ t ·⋆ ren⋆ ρ⋆ A
@@ -64,6 +81,8 @@ ren ρ⋆ ρ (error A) = error (ren⋆ ρ⋆ A)
 ren ρ⋆ ρ (builtin b) = builtin b
 ren ρ⋆ ρ (wrap A B t) = wrap (ren⋆ ρ⋆ A) (ren⋆ ρ⋆ B) (ren ρ⋆ ρ t)
 ren ρ⋆ ρ (unwrap t) = unwrap (ren ρ⋆ ρ t)
+ren ρ⋆ ρ (constr A i cs) =  constr (ren⋆ ρ⋆ A) i (ren-List ρ⋆ ρ cs) 
+ren ρ⋆ ρ (case A x cs) = case (ren⋆ ρ⋆ A) (ren ρ⋆ ρ  x) (ren-List ρ⋆ ρ cs)
 
 renT ρ⋆ ρ []       = []
 renT ρ⋆ ρ (t ∷ ts) = ren ρ⋆ ρ t ∷ renT ρ⋆ ρ ts
@@ -77,13 +96,23 @@ slift⋆ ρ zero    = ` zero
 slift⋆ ρ (suc α) = ren⋆ suc (ρ α)
 
 sub⋆ : ∀{m n} → Sub⋆ m n → ScopedTy m → ScopedTy n
+
+sub⋆-List : ∀{m n} → Sub⋆ m n → List (ScopedTy m) → List (ScopedTy n)
+sub⋆-List σ [] = []
+sub⋆-List σ (x ∷ xs) = (sub⋆ σ x) ∷ (sub⋆-List σ xs)
+
+sub⋆-ListList : ∀{m n} → Sub⋆ m n → List (List (ScopedTy m)) → List (List (ScopedTy n))
+sub⋆-ListList σ [] = []
+sub⋆-ListList σ (xs ∷ xss) = (sub⋆-List σ xs) ∷ (sub⋆-ListList σ xss)
+
 sub⋆ σ (` α)   = σ α
 sub⋆ σ (A ⇒ B) = sub⋆ σ A ⇒ sub⋆ σ B
 sub⋆ σ (Π K A) = Π K (sub⋆ (slift⋆ σ) A)
 sub⋆ σ (ƛ K A) = ƛ K (sub⋆ (slift⋆ σ) A)
 sub⋆ σ (A · B) = sub⋆ σ A · sub⋆ σ B
 sub⋆ σ (con c) = con c
 sub⋆ σ (μ A B) = μ (sub⋆ σ A) (sub⋆ σ B)
+sub⋆ σ (SOP xss) = SOP (sub⋆-ListList σ xss) 
 
 sub⋆T : ∀{m n o} → Sub⋆ m n → Tel⋆ m o → Tel⋆ n o
 sub⋆T σ⋆ []       = []
@@ -104,6 +133,11 @@ sub : ∀{m n}{v : Weirdℕ m}{w : Weirdℕ n} → Sub⋆ m n → Sub v w
 subT : ∀{m n o}{v : Weirdℕ m}{w : Weirdℕ n} → Sub⋆ m n → Sub v w
   → Tel v o → Tel w o
 
+sub-List : ∀{m n}{v : Weirdℕ m}{w : Weirdℕ n} → Sub⋆ m n → Sub v w
+  → List (ScopedTm v) → List (ScopedTm w)
+sub-List σ⋆ σ [] = []
+sub-List σ⋆ σ (x ∷ xs) = (sub σ⋆ σ x) ∷ (sub-List σ⋆ σ xs)
+
 sub σ⋆ σ (` x) = σ x
 sub σ⋆ σ (Λ K t) = Λ K (sub (slift⋆ σ⋆) (⋆slift σ) t)
 sub σ⋆ σ (t ·⋆ A) = sub σ⋆ σ t ·⋆ sub⋆ σ⋆ A
@@ -114,6 +148,9 @@ sub σ⋆ σ (error A) = error (sub⋆ σ⋆ A)
 sub σ⋆ σ (builtin b) = builtin b
 sub σ⋆ σ (wrap A B t) = wrap (sub⋆ σ⋆ A) (sub⋆ σ⋆ B) (sub σ⋆ σ t)
 sub σ⋆ σ (unwrap t) = unwrap (sub σ⋆ σ t)
+sub σ⋆ σ (constr A i cs) = constr (sub⋆ σ⋆ A) i (sub-List σ⋆ σ cs)
+sub σ⋆ σ (case A x cs) = case (sub⋆ σ⋆ A) (sub σ⋆ σ x) (sub-List σ⋆ σ cs)
+
 
 subT σ⋆ σ []       = []
 subT σ⋆ σ (t ∷ ts) = sub σ⋆ σ t ∷ subT σ⋆ σ ts
@@ -148,13 +185,27 @@ lift⋆-cong p (suc x) = cong suc (p x)
 ren⋆-cong : ∀{m n}{ρ ρ' : Ren⋆ m n}
   → (∀ x → ρ x ≡ ρ' x)
   → ∀ x → ren⋆ ρ x ≡ ren⋆ ρ' x
+
+ren⋆-cong-List :  ∀{m n}{ρ ρ' : Ren⋆ m n}
+  → (∀ x → ρ x ≡ ρ' x) 
+  → ∀ xs → ren⋆-List ρ xs ≡ ren⋆-List ρ' xs
+ren⋆-cong-List p [] = refl
+ren⋆-cong-List p (x ∷ xs) = cong₂ _∷_ (ren⋆-cong p x) (ren⋆-cong-List p xs)
+
+ren⋆-cong-ListList : ∀ {m n} {ρ ρ' : Ren⋆ m n}
+  → (∀ x → ρ x ≡ ρ' x)
+  → ∀ xss → ren⋆-ListList ρ xss ≡ ren⋆-ListList ρ' xss
+ren⋆-cong-ListList p [] = refl
+ren⋆-cong-ListList p (xs ∷ xss) = cong₂ _∷_ (ren⋆-cong-List p xs) (ren⋆-cong-ListList p xss)
+
 ren⋆-cong p (` x)       = cong ` (p x)
 ren⋆-cong p (A ⇒ B)     = cong₂ _⇒_ (ren⋆-cong p A) (ren⋆-cong p B)
 ren⋆-cong p (Π K A)     = cong (Π K) (ren⋆-cong (lift⋆-cong p) A)
 ren⋆-cong p (ƛ K A)     = cong (ƛ K) (ren⋆-cong (lift⋆-cong p) A)
 ren⋆-cong p (A · B)     = cong₂ _·_ (ren⋆-cong p A) (ren⋆-cong p B)
 ren⋆-cong p (con c)     = refl
 ren⋆-cong p (μ pat arg) = cong₂ μ (ren⋆-cong p pat) (ren⋆-cong p arg)
+ren⋆-cong p (SOP xss)   = cong SOP (ren⋆-cong-ListList p xss)
 
 slift⋆-cong : ∀{m n}{ρ ρ' : Sub⋆ m n}
   → (∀ x → ρ x ≡ ρ' x)
@@ -165,13 +216,27 @@ slift⋆-cong p (suc x) = cong (ren⋆ suc) (p x)
 sub⋆-cong : ∀{m n}{σ σ' : Sub⋆ m n}
   → (∀ x → σ x ≡ σ' x)
   → ∀ x → sub⋆ σ x ≡ sub⋆ σ' x
+
+sub⋆-cong-List :  ∀{m n}{σ σ' : Sub⋆ m n}
+  → (∀ x → σ x ≡ σ' x)
+  → ∀ xs → sub⋆-List σ xs ≡ sub⋆-List σ' xs
+sub⋆-cong-List p [] = refl
+sub⋆-cong-List p (x ∷ xs) = cong₂ _∷_ (sub⋆-cong p x) (sub⋆-cong-List p xs)
+
+sub⋆-cong-ListList : ∀{m n}{σ σ' : Sub⋆ m n}
+  → (∀ x → σ x ≡ σ' x)
+  → ∀ xss → sub⋆-ListList σ xss ≡ sub⋆-ListList σ' xss
+sub⋆-cong-ListList p [] = refl
+sub⋆-cong-ListList p (xs ∷ xss) = cong₂ _∷_ (sub⋆-cong-List p xs) (sub⋆-cong-ListList p xss)
+
 sub⋆-cong p (` x)       = p x
 sub⋆-cong p (A ⇒ B)     = cong₂ _⇒_ (sub⋆-cong p A) (sub⋆-cong p B)
 sub⋆-cong p (Π K A)     = cong (Π K) (sub⋆-cong (slift⋆-cong p) A)
 sub⋆-cong p (ƛ K A)     = cong (ƛ K) (sub⋆-cong (slift⋆-cong p) A)
 sub⋆-cong p (A · B)     = cong₂ _·_ (sub⋆-cong p A) (sub⋆-cong p B)
 sub⋆-cong p (con c)     = refl 
 sub⋆-cong p (μ pat arg) = cong₂ μ (sub⋆-cong p pat) (sub⋆-cong p arg)
+sub⋆-cong p (SOP xss)   = cong SOP (sub⋆-cong-ListList p xss)
 
 sub-cons : ∀{n n'}{w : Weirdℕ n}{w' : Weirdℕ n'} → Sub w w' → ScopedTm w' →
   Sub (S w) w'