------------------------------------------------------------------------
-- The logical relation is clsoed under reduction (in both directions).
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Erasure.LogicalRelation.Assumptions
open import Graded.Modality

module Graded.Erasure.LogicalRelation.Reduction
  {a} {M : Set a}
  {š•„ : Modality M}
  {R : Type-restrictions š•„}
  (as : Assumptions R)
  where

open Assumptions as
open Modality š•„
open Type-restrictions R

open import Definition.LogicalRelation.Simplified R

open import Definition.Untyped M as U
open import Definition.Untyped.Whnf M type-variant
open import Definition.Typed R
open import Definition.Typed.Properties R

open import Definition.Untyped.Properties M as UP using (wk-id ; wk-lift-id)

open import Graded.Erasure.Extraction.Properties š•„
open import Graded.Erasure.LogicalRelation as
open import Graded.Erasure.Target as T hiding (_āŠ¢_ā‡’_; _āŠ¢_ā‡’*_)
open import Graded.Erasure.Target.Properties as TP
open import Graded.Erasure.Target.Reasoning

open import Tools.Function
open import Tools.Nat
open import Tools.Product as Ī£
import Tools.PropositionalEquality as PE
open import Tools.Relation
open import Tools.Sum using (injā‚; injā‚‚)

private
  variable
    n : Nat
    t tā€² A : U.Term n
    v vā€² : T.Term n
    Ī“ : U.Con U.Term n

opaque

  -- The logical relation for erasure is preserved by backward
  -- "reduction" for the source term.

  sourceRedSubstTerm :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    tā€² Ā® v āˆ· A / [A] ā†’
    t ā‡› tā€² āˆ· A ā†’
    t Ā® v āˆ· A / [A]
  sourceRedSubstTerm (Levelįµ£ _) (U/Levelįµ£ ā‡’*ā†Æ) _ =
    U/Levelįµ£ ā‡’*ā†Æ
  sourceRedSubstTerm (Uįµ£ _) (U/Levelįµ£ ā‡’*ā†Æ) _ =
    U/Levelįµ£ ā‡’*ā†Æ
  sourceRedSubstTerm (Liftįµ£ā€² ā‡’*Lift āŠ©A) tā€²Ā®v tā‡›tā€² =
    sourceRedSubstTerm āŠ©A tā€²Ā®v (lower-ā‡› (conv-ā‡› tā‡›tā€² (subset* ā‡’*Lift)))
  sourceRedSubstTerm (ā„•įµ£ D) (zeroįµ£ tā€²ā‡’zero vā‡’vā€²) tā‡’tā€² =
    zeroįµ£ (trans-ā‡› (conv-ā‡› tā‡’tā€² (subset* D)) tā€²ā‡’zero) vā‡’vā€²
  sourceRedSubstTerm (ā„•įµ£ ā‡’*ā„•) (sucįµ£ tā€²ā‡’suc vā‡’vā€² num tĀ®v) tā‡’tā€² =
    sucįµ£ (trans-ā‡› (conv-ā‡› tā‡’tā€² (subset* ā‡’*ā„•)) tā€²ā‡’suc) vā‡’vā€² num tĀ®v
  sourceRedSubstTerm (Unitįµ£ D) (starįµ£ tā€²ā‡’star vā‡’star) tā‡’tā€² =
    starįµ£ (trans-ā‡› (conv-ā‡› tā‡’tā€² (subset* D)) tā€²ā‡’star) vā‡’star
  sourceRedSubstTerm (Bįµ£ā€² BMĪ  p q F G D [F] [G]) tĀ®v tā‡’tā€²
    with is-šŸ˜? p
  ... | yes PE.refl = tĀ®v .projā‚ , Ī» {a = a} āŠ¢a ā†’
    sourceRedSubstTerm ([G] āŠ¢a) (tĀ®v .projā‚‚ āŠ¢a)
      (app-ā‡› (conv-ā‡› tā‡’tā€² (subset* D)) āŠ¢a)
  ... | no pā‰¢šŸ˜ = tĀ®v .projā‚ , Ī» {a = a} āŠ¢a aĀ®w ā†’
    sourceRedSubstTerm ([G] āŠ¢a) (tĀ®v .projā‚‚ āŠ¢a aĀ®w)
      (app-ā‡› (conv-ā‡› tā‡’tā€² (subset* D)) āŠ¢a)
  sourceRedSubstTerm
    (Bįµ£ā€² (BMĪ£ _) _ _ F G D [F] [G])
    (tā‚ , tā‚‚ , tā€²ā‡’p , āŠ¢tā‚ , vā‚‚ , tā‚‚Ā®vā‚‚ , extra) tā‡’tā€² =
    tā‚ , tā‚‚ , trans-ā‡› (conv-ā‡› tā‡’tā€² (subset* D)) tā€²ā‡’p , āŠ¢tā‚ , vā‚‚ , tā‚‚Ā®vā‚‚ ,
    extra
  sourceRedSubstTerm (Idįµ£ āŠ©A) (rflįµ£ tā€²ā‡’*rfl ā‡’*ā†Æ) tā‡’tā€² =
    rflįµ£ (trans-ā‡› (conv-ā‡› tā‡’tā€² (subset* (_āŠØId_.ā‡’*Id āŠ©A))) tā€²ā‡’*rfl) ā‡’*ā†Æ
  sourceRedSubstTerm (ne record{}) ()
  sourceRedSubstTerm (Emptyįµ£ _)    ()

opaque

  -- Logical relation for erasure is preserved under a single reduction backwards on the target language term
  --
  -- Proof by induction on t Ā® vā€² āˆ· A

  targetRedSubstTerm :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    t Ā® vā€² āˆ· A / [A] ā†’
    vs T.āŠ¢ v ā‡’ vā€² ā†’
    t Ā® v āˆ· A / [A]
  targetRedSubstTerm (Levelįµ£ _) (U/Levelįµ£ ā‡’*ā†Æ) vā‡’vā€² =
    U/Levelįµ£ (T.trans vā‡’vā€² āˆ˜ā†’ ā‡’*ā†Æ)
  targetRedSubstTerm (Uįµ£ _) (U/Levelįµ£ ā‡’*ā†Æ) vā‡’vā€² =
    U/Levelįµ£ (T.trans vā‡’vā€² āˆ˜ā†’ ā‡’*ā†Æ)
  targetRedSubstTerm (Liftįµ£ā€² _ āŠ©A) tĀ®vā€² vā‡’vā€² =
    targetRedSubstTerm āŠ©A tĀ®vā€² vā‡’vā€²
  targetRedSubstTerm (ā„•įµ£ x) (zeroįµ£ tā€²ā‡’zero vā€²ā‡’zero) vā‡’vā€² = zeroįµ£ tā€²ā‡’zero (trans vā‡’vā€² vā€²ā‡’zero)
  targetRedSubstTerm (ā„•įµ£ _) (sucįµ£ tā€²ā‡’suc vā€²ā‡’suc num tĀ®v) vā‡’vā€² =
    sucįµ£ tā€²ā‡’suc (trans vā‡’vā€² vā€²ā‡’suc) num tĀ®v
  targetRedSubstTerm (Unitįµ£ x) (starįµ£ xā‚ vā€²ā‡’star) vā‡’vā€² = starįµ£ xā‚ (trans vā‡’vā€² vā€²ā‡’star)
  targetRedSubstTerm
    (Bįµ£ā€² BMĪ  p q F G D [F] [G]) (vā€²ā‡’*lam , tĀ®v) vā‡’vā€²
    with is-šŸ˜? p | Ī£.map idį¶  (T.trans vā‡’vā€²) āˆ˜ā†’ vā€²ā‡’*lam
  ... | yes PE.refl | vā‡’*lam = vā‡’*lam , Ī» āŠ¢a ā†’
    targetRedSubstTerm ([G] āŠ¢a) (tĀ®v āŠ¢a) (app-šŸ˜ā€²-subst vā‡’vā€²)
  ... | no pā‰¢šŸ˜ | vā‡’*lam = vā‡’*lam , Ī» āŠ¢a aĀ®w ā†’
    targetRedSubstTerm ([G] āŠ¢a) (tĀ®v āŠ¢a aĀ®w) (app-subst vā‡’vā€²)
  targetRedSubstTerm {A = A} {t = t} {v = v}
    [Ī£]@(Bįµ£ā€² (BMĪ£ _) p _ F G D [F] [G])
    (tā‚ , tā‚‚ , tā‡’tā€² , āŠ¢tā‚ , vā‚‚ , tā‚‚Ā®vā‚‚ , extra) vā‡’vā€² =
      tā‚ , tā‚‚ , tā‡’tā€² , āŠ¢tā‚ , vā‚‚ , tā‚‚Ā®vā‚‚
         , Ī£-Ā®-elim (Ī» _ ā†’ Ī£-Ā® F [F] tā‚ v vā‚‚ p) extra
               (Ī» vā€²ā‡’vā‚‚         ā†’ Ī£-Ā®-intro-šŸ˜ (trans vā‡’vā€² vā€²ā‡’vā‚‚))
               (Ī» vā‚ vā€²ā‡’p tā‚Ā®vā‚ ā†’ Ī£-Ā®-intro-Ļ‰ vā‚ (trans vā‡’vā€² vā€²ā‡’p) tā‚Ā®vā‚)
  targetRedSubstTerm (Idįµ£ _) (rflįµ£ tā‡’*rfl ā‡’*ā†Æ) vā‡’vā€² =
    rflįµ£ tā‡’*rfl (T.trans vā‡’vā€² āˆ˜ā†’ ā‡’*ā†Æ)
  targetRedSubstTerm (ne record{}) ()
  targetRedSubstTerm (Emptyįµ£ _)    ()

opaque

  -- Logical relation for erasure is preserved under reduction closure backwards
  -- on the target language term.
  --
  -- Proof by induction on t Ā® vā€² āˆ· A

  targetRedSubstTerm* :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    t Ā® vā€² āˆ· A / [A] ā†’
    vs T.āŠ¢ v ā‡’* vā€² ā†’
    t Ā® v āˆ· A / [A]
  targetRedSubstTerm* [A] tĀ®vā€² refl = tĀ®vā€²
  targetRedSubstTerm* [A] tĀ®vā€² (trans x vā‡’vā€²) =
    targetRedSubstTerm [A] (targetRedSubstTerm* [A] tĀ®vā€² vā‡’vā€²) x

opaque

  -- The logical relation for erasure is preserved by backward
  -- "reduction" for the source term and backward reduction for the
  -- target term.

  redSubstTerm :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    tā€² Ā® vā€² āˆ· A / [A] ā†’
    t ā‡› tā€² āˆ· A ā†’
    vs T.āŠ¢ v ā‡’ vā€² ā†’
    t Ā® v āˆ· A / [A]
  redSubstTerm [A] tā€²Ā®vā€² tā‡’tā€² vā‡’vā€² =
    targetRedSubstTerm [A] (sourceRedSubstTerm [A] tā€²Ā®vā€² tā‡’tā€²) vā‡’vā€²

opaque

  -- The logical relation for erasure is preserved by backward
  -- "reduction" for the source term and backward reduction for the
  -- target term.

  redSubstTerm* :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    tā€² Ā® vā€² āˆ· A / [A] ā†’
    t ā‡› tā€² āˆ· A ā†’
    vs T.āŠ¢ v ā‡’* vā€² ā†’
    t Ā® v āˆ· A / [A]
  redSubstTerm* [A] tā€²Ā®vā€² tā‡’tā€² vā‡’vā€² =
    targetRedSubstTerm* [A] (sourceRedSubstTerm [A] tā€²Ā®vā€² tā‡’tā€²) vā‡’vā€²

opaque

  -- The logical relation for erasure is preserved by "reduction" for
  -- the source term.

  sourceRedSubstTermā€² :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    t Ā® v āˆ· A / [A] ā†’
    t ā‡› tā€² āˆ· A ā†’
    tā€² Ā® v āˆ· A / [A]
  sourceRedSubstTermā€² (Levelįµ£ _) (U/Levelįµ£ ā‡’*ā†Æ) _ =
    U/Levelįµ£ ā‡’*ā†Æ
  sourceRedSubstTermā€² (Uįµ£ _) (U/Levelįµ£ ā‡’*ā†Æ) _ =
    U/Levelįµ£ ā‡’*ā†Æ
  sourceRedSubstTermā€² (Liftįµ£ā€² ā‡’*Lift āŠ©A) tĀ®v tā‡›tā€² =
    sourceRedSubstTermā€² āŠ©A tĀ®v (lower-ā‡› (conv-ā‡› tā‡›tā€² (subset* ā‡’*Lift)))
  sourceRedSubstTermā€² (ā„•įµ£ D) (zeroįµ£ tā‡’zero vā‡’zero) tā‡’tā€²
    with whnf-ā‡› tā‡’zero zeroā‚™ (conv-ā‡› tā‡’tā€² (subset* D))
  ... | tā€²ā‡’zero = zeroįµ£ tā€²ā‡’zero vā‡’zero
  sourceRedSubstTermā€² (ā„•įµ£ D) (sucįµ£ tā‡’suc vā‡’suc num tĀ®v) tā‡’tā€²
    with whnf-ā‡› tā‡’suc sucā‚™ (conv-ā‡› tā‡’tā€² (subset* D))
  ... | tā€²ā‡’suc = sucįµ£ tā€²ā‡’suc vā‡’suc num tĀ®v
  sourceRedSubstTermā€² (Unitįµ£ x) (starįµ£ tā‡’star vā‡’star) tā‡’tā€²
    with whnf-ā‡› tā‡’star starā‚™ (conv-ā‡› tā‡’tā€² (subset* x))
  ... | tā€²ā‡’star = starįµ£ tā€²ā‡’star vā‡’star
  sourceRedSubstTermā€²
    (Bįµ£ā€² BMĪ  p q F G D [F] [G]) tĀ®v tā‡’tā€²
    with is-šŸ˜? p
  ... | yes PE.refl = tĀ®v .projā‚ , Ī» āŠ¢a ā†’
    sourceRedSubstTermā€² ([G] āŠ¢a) (tĀ®v .projā‚‚ āŠ¢a)
      (app-ā‡› (conv-ā‡› tā‡’tā€² (subset* D)) āŠ¢a)
  ... | no pā‰¢šŸ˜ = tĀ®v .projā‚ , Ī» {a = a} āŠ¢a aĀ®w ā†’
    sourceRedSubstTermā€² ([G] āŠ¢a) (tĀ®v .projā‚‚ āŠ¢a aĀ®w)
      (app-ā‡› (conv-ā‡› tā‡’tā€² (subset* D)) āŠ¢a)
  sourceRedSubstTermā€²
    (Bįµ£ā€² (BMĪ£ _) _ _ F G D [F] [G])
    (tā‚ , tā‚‚ , tā‡’p , āŠ¢tā‚ , vā‚‚ , tā‚‚Ā®vā‚‚ , extra) tā‡’tā€² =
    tā‚ , tā‚‚
       , whnf-ā‡› tā‡’p prodā‚™ (conv-ā‡› tā‡’tā€² (subset* D))
       , āŠ¢tā‚ , vā‚‚ , tā‚‚Ā®vā‚‚ , extra
  sourceRedSubstTermā€² (Idįµ£ āŠ©A) (rflįµ£ tā‡’*rfl ā‡’*ā†Æ) tā‡’tā€² =
    rflįµ£ (whnf-ā‡› tā‡’*rfl rflā‚™ (conv-ā‡› tā‡’tā€² (subset* (_āŠØId_.ā‡’*Id āŠ©A)))) ā‡’*ā†Æ
  sourceRedSubstTermā€² (ne record{}) ()
  sourceRedSubstTermā€² (Emptyįµ£ _)    ()


private opaque

  -- Some lemmas used below.

  Ī -lemma :
    vs T.āŠ¢ v ā‡’ vā€² ā†’
    (āˆƒ Ī» vā€³ ā†’ vs T.āŠ¢ v ā‡’* T.lam vā€³) ā†’
    (āˆƒ Ī» vā€³ ā†’ vs T.āŠ¢ vā€² ā‡’* T.lam vā€³)
  Ī -lemma vā‡’vā€² (_ , vā‡’*lam)
    with red*Det vā‡’*lam (T.trans vā‡’vā€² T.refl)
  ā€¦ | injā‚ lamā‡’*vā€² rewrite Valueā†’ā‡’*ā†’ā‰” T.lam lamā‡’*vā€² = _ , T.refl
  ā€¦ | injā‚‚ vā€²ā‡’*lam = _ , vā€²ā‡’*lam

  ā‡’*ā†Æā†’ā‡’ā†’ā‡’*ā†Æ :
    (str PE.ā‰” strict ā†’ vs T.āŠ¢ v ā‡’* ā†Æ) ā†’ vs T.āŠ¢ v ā‡’ vā€² ā†’
    str PE.ā‰” strict ā†’ vs T.āŠ¢ vā€² ā‡’* ā†Æ
  ā‡’*ā†Æā†’ā‡’ā†’ā‡’*ā†Æ {vā€²} vā‡’*ā†Æ vā‡’vā€² ā‰”strict =
    case red*Det (vā‡’*ā†Æ ā‰”strict) (T.trans vā‡’vā€² T.refl) of Ī» where
      (injā‚‚ vā€²ā‡’*ā†Æ) ā†’ vā€²ā‡’*ā†Æ
      (injā‚ ā†Æā‡’*vā€²) ā†’
        vā€²  ā‰”āŸØ ā†Æ-noRed ā†Æā‡’*vā€² āŸ©ā‡’
        ā†Æ   āˆŽā‡’

opaque

  -- The logical relation for erasure is preserved under reduction of
  -- the target language term.

  targetRedSubstTerm*ā€² :
    ([A] : ts Ā» Ī” āŠØ A) ā†’ t Ā® v āˆ· A / [A] ā†’
    vs T.āŠ¢ v ā‡’* vā€² ā†’ t Ā® vā€² āˆ· A / [A]

  -- Logical relation for erasure is preserved under one reduction step on the target language term
  -- If t Ā® v āˆ· A and v ā‡’ vā€²  then t Ā® vā€² āˆ· A
  --
  -- Proof by induction on t Ā® v āˆ· A

  targetRedSubstTermā€² : ([A] : ts Ā» Ī” āŠØ A) ā†’ t Ā® v āˆ· A / [A]
                      ā†’ vs T.āŠ¢ v ā‡’ vā€² ā†’ t Ā® vā€² āˆ· A / [A]
  targetRedSubstTermā€² (Levelįµ£ _) (U/Levelįµ£ vā‡’*ā†Æ) vā‡’vā€² =
    U/Levelįµ£ (ā‡’*ā†Æā†’ā‡’ā†’ā‡’*ā†Æ vā‡’*ā†Æ vā‡’vā€²)
  targetRedSubstTermā€² (Uįµ£ _) (U/Levelįµ£ vā‡’*ā†Æ) vā‡’vā€² =
    U/Levelįµ£ (ā‡’*ā†Æā†’ā‡’ā†’ā‡’*ā†Æ vā‡’*ā†Æ vā‡’vā€²)
  targetRedSubstTermā€² (Liftįµ£ā€² _ āŠ©A) tĀ®v vā‡’vā€² =
    targetRedSubstTermā€² āŠ©A tĀ®v vā‡’vā€²
  targetRedSubstTermā€² (ā„•įµ£ x) (zeroįµ£ xā‚ vā‡’zero) vā‡’vā€² with red*Det vā‡’zero (T.trans vā‡’vā€² T.refl)
  ... | injā‚ xā‚‚ rewrite zero-noRed xā‚‚ = zeroįµ£ xā‚ T.refl
  ... | injā‚‚ xā‚‚ = zeroįµ£ xā‚ xā‚‚
  targetRedSubstTermā€² (ā„•įµ£ _) (sucįµ£ tā‡’suc vā‡’suc num tĀ®v) vā‡’vā€²
    with red*Det vā‡’suc (T.trans vā‡’vā€² T.refl)
  ... | injā‚ sucā‡’* rewrite suc-noRed sucā‡’* = sucįµ£ tā‡’suc T.refl num tĀ®v
  ... | injā‚‚ ā‡’*suc = sucįµ£ tā‡’suc ā‡’*suc num tĀ®v
  targetRedSubstTermā€² (Unitįµ£ x) (starįµ£ xā‚ vā‡’star) vā‡’vā€² with red*Det vā‡’star (T.trans vā‡’vā€² T.refl)
  ... | injā‚ xā‚‚ rewrite star-noRed xā‚‚ = starįµ£ xā‚ T.refl
  ... | injā‚‚ xā‚‚ = starįµ£ xā‚ xā‚‚
  targetRedSubstTermā€²
    (Bįµ£ā€² BMĪ  p q F G D [F] [G]) tĀ®v vā‡’vā€²
    with is-šŸ˜? p
  ... | yes PE.refl = Ī -lemma vā‡’vā€² āˆ˜ā†’ tĀ®v .projā‚ , Ī» āŠ¢a ā†’
    targetRedSubstTermā€² ([G] āŠ¢a) (tĀ®v .projā‚‚ āŠ¢a) (app-šŸ˜ā€²-subst vā‡’vā€²)
  ... | no pā‰¢šŸ˜ = Ī -lemma vā‡’vā€² āˆ˜ā†’ tĀ®v .projā‚ , Ī» āŠ¢a aĀ®w ā†’
    targetRedSubstTermā€² ([G] āŠ¢a) (tĀ®v .projā‚‚ āŠ¢a aĀ®w) (T.app-subst vā‡’vā€²)
  targetRedSubstTermā€²
    {vā€² = vā€²}
    (Bįµ£ā€² (BMĪ£ _) p _ F G D [F] [G])
    (tā‚ , tā‚‚ , tā‡’tā€² , āŠ¢tā‚ , vā‚‚ , tā‚‚Ā®vā‚‚ , extra) vā‡’vā€² =
    let [Gtā‚] = [G] āŠ¢tā‚
    in  tā‚ , tā‚‚ , tā‡’tā€² , āŠ¢tā‚
        , Ī£-Ā®-elim
           (Ī» _ ā†’ āˆƒ Ī» vā‚‚ ā†’ (tā‚‚ Ā® vā‚‚ āˆ· G U.[ tā‚ ]ā‚€ / [Gtā‚])
                         Ɨ Ī£-Ā® F _ tā‚ vā€² vā‚‚ p)
           extra
           (Ī» vā‡’vā‚‚ pā‰”šŸ˜ ā†’ case red*Det vā‡’vā‚‚ (trans vā‡’vā€² refl) of Ī» where
             (injā‚ vā‚‚ā‡’vā€²) ā†’ vā€² , targetRedSubstTerm*ā€² [Gtā‚] tā‚‚Ā®vā‚‚ vā‚‚ā‡’vā€²
                               , Ī£-Ā®-intro-šŸ˜ refl pā‰”šŸ˜
             (injā‚‚ vā€²ā‡’vā‚‚) ā†’ vā‚‚ , tā‚‚Ā®vā‚‚ , Ī£-Ā®-intro-šŸ˜ vā€²ā‡’vā‚‚ pā‰”šŸ˜)
           Ī» vā‚ vā‡’p tā‚Ā®vā‚ pā‰¢šŸ˜ ā†’ vā‚‚ , tā‚‚Ā®vā‚‚ , (case red*Det vā‡’p (trans vā‡’vā€² refl) of Ī» where
             (injā‚ pā‡’vā€²) ā†’ case prod-noRed pā‡’vā€² of Ī» where
               PE.refl ā†’ Ī£-Ā®-intro-Ļ‰ vā‚ refl tā‚Ā®vā‚ pā‰¢šŸ˜
             (injā‚‚ vā€²ā‡’p) ā†’ Ī£-Ā®-intro-Ļ‰ vā‚ vā€²ā‡’p tā‚Ā®vā‚ pā‰¢šŸ˜)

  targetRedSubstTermā€² (Idįµ£ _) (rflįµ£ tā‡’*rfl vā‡’*ā†Æ) vā‡’vā€² =
    rflįµ£ tā‡’*rfl (ā‡’*ā†Æā†’ā‡’ā†’ā‡’*ā†Æ vā‡’*ā†Æ vā‡’vā€²)
  targetRedSubstTermā€² (ne record{}) ()
  targetRedSubstTermā€² (Emptyįµ£ _)    ()


  targetRedSubstTerm*ā€² [A] tĀ®v refl = tĀ®v
  targetRedSubstTerm*ā€² [A] tĀ®v (trans x vā‡’vā€²) =
    targetRedSubstTerm*ā€² [A] (targetRedSubstTermā€² [A] tĀ®v x) vā‡’vā€²

opaque

  -- The logical relation for erasure is preserved by "reduction" for
  -- the source term and reduction for the target term.

  redSubstTermā€² :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    t Ā® v āˆ· A / [A] ā†’
    t ā‡› tā€² āˆ· A ā†’
    vs T.āŠ¢ v ā‡’ vā€² ā†’
    tā€² Ā® vā€² āˆ· A / [A]
  redSubstTermā€² [A] tĀ®v tā‡’tā€² vā‡’vā€² =
    targetRedSubstTermā€² [A] (sourceRedSubstTermā€² [A] tĀ®v tā‡’tā€²) vā‡’vā€²

opaque

  -- The logical relation for erasure is preserved by "reduction" for
  -- the source term and reduction for the target term.

  redSubstTerm*ā€² :
    ([A] : ts Ā» Ī” āŠØ A) ā†’
    t Ā® v āˆ· A / [A] ā†’
    t ā‡› tā€² āˆ· A ā†’
    vs T.āŠ¢ v ā‡’* vā€² ā†’
    tā€² Ā® vā€² āˆ· A / [A]
  redSubstTerm*ā€² [A] tĀ®v tā‡’tā€² vā‡’vā€² =
    targetRedSubstTerm*ā€² [A] (sourceRedSubstTermā€² [A] tĀ®v tā‡’tā€²) vā‡’vā€²