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

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

module LogRel.Gen
  {{ Α : Set }}    -- type level constants
  {{ C : Set }}    -- term level constants

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

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

  where

import SyntaxRew
open SyntaxRew -- using (MT ; go ; [)
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

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

  {{ Κ }}    -- proof term constants
  
import LogRel
open LogRel
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

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

  {{ Κ }}    -- proof term constants



import SmlSem
open SmlSem 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

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

  {{ Κ }}    -- proof term constants
  using (∀gen)



log-gen' : ∀ {S : Sig} {P : Prog} {Γ' : Ctx} {e : MT} {G : Go} {x : Var} {A : T} →
      logrel S P (Γ' , x ∷ A) e (go G) →
      logrel S P Γ' e (go (∀Go x A G))

log-gen' log = l∀R (log-subst (log-weaken-sig {!log!} {!!}) {!!})



log-gen : ∀ {S : Sig} {P : Prog} {Γ' : Ctx} {e : PT} {G : Go} →
      logrel S P Γ' (inMT e) (go G) →
      logrel S P · (inMT e) (go (∀gen Γ' G))

log-gen {Γ' = ·} log = log
log-gen {Γ' = Γ' , x ∷ A} log = log-gen {Γ' = Γ'} (log-gen' log)