{-# OPTIONS --allow-unsolved-metas #-} 

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)


module SmlSem
  {{ Α : Set }}    -- type level constants
  {{ C : Set }}    -- term level constants

  {{ Var : Set }}  -- variables
  {{ decEqVar : Decidable (_≡_ {A = Var}) }}

  {{  Κ : Set }}   -- proof term constants

  where

{-
import LF
open LF --{{Α}} {{C}} {{T}} {{K}} {{Var}} {{UVar}} 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }} 



import Syntax
open Syntax --{{Α}} {{C}} {{T}} {{K}} {{Var}} {{UVar}} 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }}
  
  {{ Κ }}    -- proof term constants
-}

import SyntaxRew
open SyntaxRew --{{Α}} {{C}} {{T}} {{K}} {{Var}} {{UVar}} 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }}
    
  {{ Κ }}    -- proof term constants
  public


-- small step operational semantics
mutual
  data _+_⊢_∣_~>_∣_ : Sig → Prog → Ctx → MT → Ctx → MT → Set where

    sdec : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC} {e : MT} {A : T} {κ : Κ} {D : De} →
      S + P ⊢ Γ ∣ (C [ go (at A) ]) ~ (symbM κ) ∷ D ~> Γ' ∣ e ->
      κ ∷ D ∈P P → {- w.f. of P -} 
      S + P ⊢ Γ ∣ (C [ go (at A) ]) ~> Γ' ∣ e

    s∃R : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC } {x : Var} {A : T} {G : Go} {e : MT}  →
      S + P ⊢ Γ , x ∷ A ∣ C [ < var x , go G >M ] ~> Γ' ∣ e →
      S + P ⊢ Γ ∣ (C [ go (∃Go x A G) ]) ~> Γ' ∣ e
      
    s⇒R : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC} { e' : MT} {G : Go} {D : De} {κ : Κ}→
      S + P , κ ∷ D ⊢ Γ ∣ (C [ lamM κ (go G) ]) ~> Γ' ∣ e' →
      S + P ⊢ Γ ∣ (C [ go (D ⇒ G) ]) ~> Γ' ∣ e' 

    s∀R : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC} {e : MT} {G : Go} {x : Var} {A : T} →
      S + P ⊢ Γ , x ∷ A ∣ (C [ go G ]) ~> Γ' ∣ e →
      S + P ⊢ Γ ∣ (C [ go (∀Go x A G) ]) ~> Γ' ∣ e
    
  data _+_⊢_∣_~_∷_~>_∣_ : Sig → Prog → Ctx → MT → MT → De → Ctx → MT → Set where

    unif : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {A A' : T} {e : MT} {C : RewC } → 

      -- TODO check unification with prefix
      (σ : Θ S Γ Γ') →
      (S + Γ' ⊢ (σ ΘT A) ≡T (σ ΘT A') ∷ o) →
      S ⊢prog P → 
      S + P ⊢ Γ ∣ (C [ go (at A) ]) ~ e ∷ at A' ~> Γ' ∣ (C [ e ])

    s⇒L : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC} {e : MT} {e₁ : MT} {D : De} {A A₁ : T} →
      S + P ⊢ Γ ∣ (C [ go (at A) ]) ~ e₁ apM (go (at A₁)) ∷ D ~> Γ' ∣ e →
      S + P ⊢ Γ ∣ (C [ go (at A) ]) ~ e₁ ∷ at A₁ ⇒ D ~> Γ' ∣ e


    s∀L : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC} {e e' : MT} {x : Var} {Y : Var} {D : De} {A₁ A₂ : T} →
      S + P ⊢ Γ , x ∷ A₁ ∣ (C [ go (at A₂) ]) ~ e ∷ D ~> Γ' ∣ e' →
      S + P ⊢ Γ ∣ (C [ go (at A₂) ]) ~ e ∷ ∀De x A₁ D ~> Γ' ∣ e'


import LF
open LF using ( ,∷-wfctx )

preserves-wf :  {S : Sig} {P : Prog} {Γ Γ' : Ctx} {e e' : MT} →
      S + P ⊢ Γ ∣ e ~> Γ' ∣ e' ->
      S ⊢ Γ

preserves-wf-dec :  {S : Sig} {P : Prog} {Γ Γ' : Ctx}  {e e' e₁ : MT}  {D : De} →
      S + P ⊢ Γ ∣ e ~ e₁ ∷ D ~> Γ' ∣ e' ->
      S ⊢ Γ

preserves-wf (sdec smldec x) = preserves-wf-dec smldec
preserves-wf (s∃R sml)
  with preserves-wf sml
preserves-wf (s∃R sml) | ,∷-wfctx res = res 

preserves-wf (s⇒R sml) = preserves-wf sml
preserves-wf (s∀R sml)
  with preserves-wf sml
preserves-wf (s∀R sml) | ,∷-wfctx res = res 

preserves-wf-dec (unif σ x y) = {!!}

preserves-wf-dec (s⇒L smldec) = preserves-wf-dec smldec
preserves-wf-dec (s∀L smldec)
  with preserves-wf-dec smldec
preserves-wf-dec (s∀L smldec) | ,∷-wfctx res = res


preserves-wf' :  {S : Sig} {P : Prog} {Γ Γ' : Ctx} {e e' : MT} →
      S + P ⊢ Γ ∣ e ~> Γ' ∣ e' ->
      S ⊢ Γ'

preserves-wf-dec' :  {S : Sig} {P : Prog} {Γ Γ' : Ctx}  {e e' e₁ : MT}  {D : De} →
      S + P ⊢ Γ ∣ e ~ e₁ ∷ D ~> Γ' ∣ e' ->
      S ⊢ Γ'

preserves-wf' (sdec smldec x) = preserves-wf-dec' smldec
preserves-wf' (s∃R sml) = preserves-wf' sml
preserves-wf' (s⇒R sml) = preserves-wf' sml
preserves-wf' (s∀R sml) = preserves-wf' sml

preserves-wf-dec' (unif σ x wfP) = impl-val-ctx x
preserves-wf-dec' (s⇒L smldec) = preserves-wf-dec' smldec
preserves-wf-dec' (s∀L smldec) = preserves-wf-dec' smldec


sml-val-prog  : {S : Sig} {P : Prog} {Γ Γ' : Ctx}  {ê ê'  : MT} →
   S + P ⊢ Γ ∣ ê ~> Γ' ∣ ê' →
   S ⊢prog P

smldec-val-prog : {S : Sig} {P : Prog} {Γ Γ' : Ctx} { ê ê' ê₁ : MT}  {D₁ : De} →
  S + P ⊢ Γ ∣ ê ~ ê₁ ∷ D₁ ~> Γ' ∣ ê' →
  S ⊢prog P

sml-val-prog (sdec x x₁) = smldec-val-prog x
sml-val-prog (s∃R sml) = sml-val-prog sml
sml-val-prog (s⇒R sml) with (sml-val-prog sml)
... | _⊢prog_.,∷-prog wfP _ _ = wfP
sml-val-prog (s∀R sml) = sml-val-prog sml

smldec-val-prog (unif σ x wfP) = wfP
smldec-val-prog (s⇒L smldec) = smldec-val-prog smldec
smldec-val-prog (s∀L smldec) = smldec-val-prog smldec



open import Function


open import Data.Product using (∃₂ ; _×_ ; _,_ )
open import Relation.Binary.PropositionalEquality using ( refl ; cong )



{- view on sml derivation -}

view-C : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC } {e ê ê'  : MT} →
  ê ≡ C [ ê' ] →
  S + P ⊢ Γ ∣ ê ~> Γ' ∣ e →
  ∃₂ (λ e' (θ : Θ S Γ Γ') → ( e ≡ (θ ΘC C) [ e' ]) × S + P ⊢ Γ ∣ ê' ~> Γ' ∣ e')

view-C-dec : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {C : RewC } {e ê ê' ê₁ : MT}
  {D₁ : De} →
  ê ≡ C [ ê' ] →
  S + P ⊢ Γ ∣ ê ~ ê₁ ∷ D₁ ~> Γ' ∣ e →
  ∃₂ (λ e' (θ : Θ S Γ Γ') → ( e ≡ (θ ΘC C) [ e' ]) × S + P ⊢ Γ ∣ ê' ~ ê₁ ∷ D₁ ~> Γ' ∣ e')

{- part 1 -}




view-C {C = ●} {e} refl (sdec {C = ●} smldec x )
  with view-C-dec {C = ●} refl smldec
... | e' , θ , refl , smldec' = e' , θ , refl , sdec smldec' x

view-C {C = SyntaxRew.●} {e} refl (sdec {C = x SyntaxRew.ap C} smldec x')
  with view-C-dec {C = ●} refl smldec
... | e' , θ , refl , smldec' = e' , θ , refl , sdec smldec' x'

view-C {C = SyntaxRew.●} {e} refl (sdec {C = SyntaxRew.< x , C >} smldec x')
  with view-C-dec {C = ●} refl smldec
... | e' , θ , refl , smldec' = e' , θ , refl , sdec smldec' x'

view-C {C = SyntaxRew.●} {e} refl (sdec {C = SyntaxRew.lam x C} smldec x')
  with view-C-dec {C = ●} refl smldec
... | e' , θ , refl , smldec' = e' , θ , refl , sdec smldec' x'


view-C {C = SyntaxRew.●} {e} refl (s∃R {C = SyntaxRew.●} sml)
  with view-C {C = ● } refl sml
... | e'' , θ , refl , sml' = e'' , weaken θ , refl , s∃R sml

view-C {C = SyntaxRew.●} {e} refl (s∃R {C = x SyntaxRew.ap C} sml) 
  with view-C {C = ● } refl sml
... | e'' , θ , refl , sml' = e'' , weaken θ , refl , s∃R sml

view-C {C = SyntaxRew.●} {e} refl (s∃R {C = SyntaxRew.< x , C >} sml)
  with view-C {C = ● } refl sml
... | e'' , θ , refl , sml' = e'' , weaken θ , refl , s∃R sml

view-C {C = SyntaxRew.●} {e} refl (s∃R {C = SyntaxRew.lam x C} sml)
  with view-C {C = ● } refl sml
... | e'' , θ , refl , sml' = e'' , weaken θ , refl , s∃R sml

view-C {C = SyntaxRew.●} {e} refl (s⇒R {C = SyntaxRew.●} sml)
  with view-C {C = ● } refl sml
... | e'' , θ , refl , sml' = e , θ , refl , s⇒R sml'

view-C {C = SyntaxRew.●} {e} refl (s⇒R {C = e' SyntaxRew.ap C} sml)
  with view-C {C = ●} refl sml
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒R sml'

view-C {C = SyntaxRew.●} {e} refl (s⇒R {C = SyntaxRew.< x , C >} sml)
  with view-C {C = ●} refl sml
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒R sml'

view-C {C = SyntaxRew.●} {e} refl (s⇒R {C = SyntaxRew.lam x C} sml)
  with view-C {C = ●} refl sml
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒R sml'


view-C {C = SyntaxRew.●} {e} refl (s∀R sml)
  with view-C {C = ●} refl sml
... | e'' , θ , refl , sml' = e'' , weaken θ , refl , s∀R  sml 



view-C {C = e ap C₁} {ê' = ê'} () (sdec {C = ●} _ _)
view-C {C = e ap C₁} {ê' = ê'} eq (sdec {C = e' ap C₂} sml x')
  with inspect-apM eq
... | refl , eq'
  with unique-RewC-Go {C₂ = e ap C₁} eq
... | C' , refl , eq''   
  with view-C-dec {C = e' ap C₁} (cong (_apM_ e') eq') sml
... | e'' , θ , refl , sml' = e'' , θ , refl , sdec sml' x'

view-C {C = e ap C₁} {ê' = ê'} () (sdec {C = < x₂ , C₂ >} _ _)
view-C {C = e ap C₁} {ê' = ê'} () (sdec {C = lam x₂ C₂} _ _)

view-C {C = e ap C₁} () (s∃R {C = ●} sml)
view-C {C = e ap C₁} {ê' = ê'} eq (s∃R {C = e' ap C₂} sml)
  with inspect-apM eq
... | refl , eq' 
  with unique-RewC-Go {C₂ = e ap C₁}  eq
... | C' , refl , eq''
  with view-C {C = e' ap C₁ }  eq''   sml
... | e'' , θ , refl , sml' = e'' , weaken θ , {!!} , s∃R sml'

view-C {C = e ap C₁} () (s∃R {C = < x , C₂ >} sml)
view-C {C = e ap C₁} () (s∃R {C = lam x C₂} sml)

view-C {C = e ap C₁} () (s⇒R {C = ●} sml)
view-C {C = e ap C₁} {ê' = ê'} eq (s⇒R {C = x ap C₂} {κ = κ}  sml)
  with inspect-apM eq
... | refl , eq'
  with unique-RewC-Go {C₂ = e ap C₁} eq
... | C' , refl , eq''
  with view-C {C = e ap C₁} eq'' sml
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒R sml'

view-C {C = e ap C₁} () (s⇒R {C = < x , C₂ >} sml)
view-C {C = e ap C₁} () (s⇒R {C = lam x C₂} sml)

view-C {C = e ap C₁} () (s∀R {C = ●} sml)
view-C {C = e ap C₁} {ê' = ê'} eq (s∀R {C = x ap C₂} sml)
  with inspect-apM  eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C {C = e ap C₁}
    (eq') sml
... | e'' , θ , refl , sml' = e'' , weaken θ , {!!} , s∀R sml'
view-C {C = e ap C₁} () (s∀R {C = < x , C₂ >} sml)
view-C {C = e ap C₁} () (s∀R {C = lam x C₂} sml)

view-C {C = < M , C₁ >} {ê' = ê'} () (sdec {C = ●} _ _)
view-C {C = < M , C₁ >} {ê' = ê'} () (sdec {C = x₂ ap C₂} _ _)
view-C {C = < M , C₁ >} {ê' = ê'} eq (sdec {C = < x₂ , C₂ >} x x')
  with inspect-<>M eq
... | refl , eq' 
  with unique-RewC-Go {ê = ê'}  eq
... | C' , refl , eq''
  with view-C-dec
    {C = < M , C₁ > } 
    (eq'') x
... | e'' , θ , refl , sml' = e'' , θ , refl , sdec sml' x'
view-C {C = < M , C₁ >} {ê' = ê'} () (sdec {C = lam x₂ C₂} x _)

view-C {C = < M , C₁ >} {ê' = ê'} () (s∃R {C = ●} sml)
view-C {C = < M , C₁ >} {ê' = ê'} () (s∃R {C = x ap C₂} sml)
view-C {C = < M , C₁ >} {ê' = ê'} eq (s∃R {C = < x , C₂ >} sml)
  with inspect-<>M  eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C {C = < M , C₁ >}
    (eq') sml
... | e'' , θ , refl , sml' = e'' , weaken θ , {!!} , s∃R sml'
view-C {C = < M , C₁ >} {ê' = ê'} () (s∃R {C = lam x C₂} sml)

view-C {C = < M , C₁ >} {ê' = ê'} () (s⇒R {C = ●} sml)
view-C {C = < M , C₁ >} {ê' = ê'} () (s⇒R {C = x₁ ap C₂} sml)
view-C {C = < M , C₁ >} {ê' = ê'} eq (s⇒R {C = < x₁ , C₂ >} sml)
  with inspect-<>M  eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq' 
  with view-C {C = < M , C₁ >}
    (eq') sml
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒R sml'
view-C {C = < M , C₁ >} {ê' = ê'} () (s⇒R {C = lam x₁ C₂} sml)

view-C {C = < M , C₁ >} {ê' = ê'} () (s∀R {C = ●} sml)
view-C {C = < M , C₁ >} {ê' = ê'} () (s∀R {C = x ap C₂} sml)
view-C {C = < M , C₁ >} {ê' = ê'} eq (s∀R {C = < x , C₂ >} sml)
  with inspect-<>M  eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C {C = < M , C₁ >}
    (eq') sml
... | e'' , θ , refl , sml' = e'' , weaken θ , {!!} , s∀R sml'
view-C {C = < M , C₁ >} {ê' = ê'} () (s∀R {C = lam x C₂} sml)

view-C {C = lam κ C₁} {ê' = ê'} () (sdec {C = ●} _ _)
view-C {C = lam κ C₁} {ê' = ê'} () (sdec {C = x₂ ap C₂} _ _)
view-C {C = lam κ C₁} {ê' = ê'} () (sdec {C = < x₂ , C₂ >} _ _)
view-C {C = lam κ C₁} {ê' = ê'} eq (sdec {C = lam x₂ C₂} x x')
  with inspect-lamM eq
... | refl , eq' 
  with unique-RewC-Go {ê = ê'}  eq
... | C' , refl , eq''
  with view-C-dec
    {C = lam κ C₁ } 
    (eq'') x
... | e'' , θ , refl , sml' = e'' , θ , refl , sdec sml' x'

view-C {C = lam κ C₁} {ê' = ê'} () (s∃R {C = ●} sml)
view-C {C = lam κ C₁} {ê' = ê'} () (s∃R {C = x ap C₂} sml)
view-C {C = lam κ C₁} {ê' = ê'} () (s∃R {C = < x , C₂ >} sml)
view-C {C = lam κ C₁} {ê' = ê'} eq (s∃R {C = lam κ' C₂} sml)
  with inspect-lamM  eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C {C = lam κ C₁ }
    eq' sml
... | e'' , θ , refl , sml' = e'' , weaken θ , cong (lamM _ ) {!!} , s∃R sml'

view-C {C = lam κ C₁} {ê' = ê'} () (s⇒R {C = ●} sml)
view-C {C = lam κ C₁} {ê' = ê'} () (s⇒R {C = e ap C₂} sml)
view-C {C = lam κ C₁} {ê' = ê'} () (s⇒R {C = < M , C₂ >} sml)
view-C {C = lam κ C₁} {ê' = ê'} eq (s⇒R {C = lam κ' C₂} sml)
  with inspect-lamM  eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C {C = lam κ C₁ }
    (eq') sml
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒R sml'

view-C {C = lam κ C₁} {ê' = ê'} () (s∀R {C = ●} sml)
view-C {C = lam κ C₁} {ê' = ê'} () (s∀R {C = x ap C₂} sml)
view-C {C = lam κ C₁} {ê' = ê'} () (s∀R {C = < x , C₂ >} sml)
view-C {C = lam κ C₁} {ê' = ê'} eq (s∀R {C = lam x C₂} sml)
  with inspect-lamM  eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C {C = lam κ C₁ }
    (eq') sml
... | e'' , θ , refl , sml' = e'' , weaken θ , cong (lamM _) {!!} , s∀R sml'


{- part 2 -}


open Relation.Binary.PropositionalEquality using (subst ; subst₂ ; sym)

view-C-dec {C = ●} {.(C₁ [ ê₁ ])} {ê₁ = ê₁} refl (unif {C = C₁} σ y z)
  = C₁ [ ê₁ ] , σ , refl , unif  σ y z
  
view-C-dec {C = ●} {e} refl (s⇒L {C = C₁} smldec)
  with view-C-dec {C = ●} refl smldec
... | e'' , θ , refl , smldec' = e'' , θ , refl , s⇒L smldec

view-C-dec {C = ●} {e} refl (s∀L smldec)
  with view-C-dec {C = ●} refl smldec
... | e'' , θ , refl , smldec' = e'' , weaken θ , refl , s∀L smldec


view-C-dec {C = x ap C₁} {.(C₂ [ ê₁ ])} {.(C₂ [ go (at A) ])} {ê₁ = ê₁} eq (unif {A = A} {C = C₂} σ wf z)
  with unique-RewC-Go' {C₁ = C₂} {C₂ = x ap C₁} {ê' = ê₁} eq
... |  C' , refl , res = C' [ ê₁ ] , σ , {!σ-lift res!} , unif σ wf z


view-C-dec {C = x ap C₁} {e} {.(go (at _))} () (s⇒L {C = ●} smldec)
view-C-dec {C = x ap C₁} {e} {ê' = ê'} eq (s⇒L {C = x₁ ap C₂} smldec)
  with inspect-apM eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C-dec {C = x ap C₁ }
    (eq') smldec
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒L sml'

view-C-dec {C = x ap C₁} () (s⇒L {C = < x₁ , C₂ >} smldec)
view-C-dec {C = x ap C₁} () (s⇒L {C = lam x₁ C₂} smldec)

view-C-dec {C = x ap C₁} {ê' = ê'} () (s∀L {C = ●} smldec)
view-C-dec {C = x ap C₁} {ê' = ê'} eq (s∀L {C = x₁ ap C₂} smldec)
  with inspect-apM eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C-dec {C = x ap C₁ }
    (eq') smldec
... | e'' , θ , refl , sml' = e'' , weaken θ , {!!} , s∀L sml'

view-C-dec {C = x ap C₁} {ê' = ê'} () (s∀L {C = < x₁ , C₂ >} smldec)
view-C-dec {C = x ap C₁} {ê' = ê'} () (s∀L {C = lam x₁ C₂} smldec)

view-C-dec {C = < x , C₁ >} {ê' = ê'} {ê₁ = ê₁} eq (unif {C = C₂} σ wf z)
  with unique-RewC-Go' {ê = ê'} {ê' = ê₁} eq
... |  C' , refl , res = C' [ ê₁ ] , σ , {!lift-σ res!} , unif σ wf z


view-C-dec {C = < x , C₁ >} {ê' = ê'} () (s⇒L {C = ●} smldec)
view-C-dec {C = < x , C₁ >} {ê' = ê'} () (s⇒L {C = x₁ ap C₂} smldec)
view-C-dec {C = < x , C₁ >} {ê' = ê'} eq (s⇒L {C = < x₁ , C₂ >} smldec)
  with inspect-<>M eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C-dec {C = < x₁ , C₁ > }
    (eq') smldec
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒L sml'

view-C-dec {C = < x , C₁ >} {ê' = ê'} () (s⇒L {C = lam x₁ C₂} smldec)

view-C-dec {C = < x , C₁ >} {ê' = ê'} () (s∀L {C = ●} smldec)
view-C-dec {C = < x , C₁ >} {ê' = ê'} () (s∀L {C = x₁ ap C₂} smldec)
view-C-dec {C = < x , C₁ >} {ê' = ê'} eq (s∀L {C = < x₁ , C₂ >} smldec)
  with inspect-<>M eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C-dec {C = < x₁ , C₁ > }
    (eq') smldec
... | e'' , θ , refl , sml' = e'' , weaken θ , {!!} , s∀L sml'

view-C-dec {C = < x , C₁ >} {ê' = ê'} () (s∀L {C = lam x₁ C₂} smldec)

view-C-dec {C = lam x C₁} {ê' = ê'} {ê₁ = ê₁} eq (unif {C = C₂} θ wf z)
  with unique-RewC-Go' {C₁ = C₂} {C₂ = lam x C₁} {ê' = ê₁} eq
... |  C' , refl , res = C' [ ê₁ ] , θ , {!σ-lift!} , unif θ wf z

view-C-dec {C = lam x C₁} {ê' = ê'} () (s⇒L {C = ●} smldec)
view-C-dec {C = lam x C₁} {ê' = ê'} () (s⇒L {C = x₁ ap C₂} smldec)
view-C-dec {C = lam x C₁} {ê' = ê'} () (s⇒L {C = < x₁ , C₂ >} smldec)
view-C-dec {C = lam x C₁} {ê' = ê'} eq (s⇒L {C = lam x₁ C₂} smldec)
  with inspect-lamM eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C-dec {C = lam x₁ C₁ }
    (eq') smldec
... | e'' , θ , refl , sml' = e'' , θ , refl , s⇒L sml'

view-C-dec {C = lam x C₁} {ê' = ê'} () (s∀L {C = ●} smldec)
view-C-dec {C = lam x C₁} {ê' = ê'} () (s∀L {C = e ap C₂} smldec)
view-C-dec {C = lam x C₁} {ê' = ê'} () (s∀L {C = < M , C₂ >} smldec)
view-C-dec {C = lam x C₁} {ê' = ê'} eq (s∀L {C = lam κ C₂} smldec)
  with inspect-lamM eq
... | refl , _
  with unique-RewC-Go {ê = ê'} eq
... | C' , refl , eq'
  with view-C-dec {C = lam κ C₁ }
    (eq') smldec
... | e'' , θ , refl , sml' = e'' , weaken θ , cong (lamM _) {!!} , s∀L sml'


∀gen : Ctx → Go → Go

∀gen · G = G
∀gen (Γ , x ∷ A) G = ∀gen Γ (∀Go x A G)


∀genMT : Ctx → MT → MT

∀genMT Γ (symbM κ) = symbM κ
∀genMT Γ (go G) = go ( ∀gen Γ G)
∀genMT Γ (ê apM ê₁) = (∀genMT Γ ê) apM (∀genMT Γ ê₁)
∀genMT Γ < M , ê >M = < M , (∀genMT Γ ê) >M
∀genMT Γ (lamM κ ê) = lamM κ (∀genMT Γ ê)