------------------------------------------------------------------------
-- Validity for natural numbers
------------------------------------------------------------------------

open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.LogicalRelation.Substitution.Introductions.Nat
  {a} {M : Set a}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  ⦃ eqrel : EqRelSet R ⦄
  where

open EqRelSet eqrel
open Type-restrictions R

open import Definition.LogicalRelation R
open import Definition.LogicalRelation.Hidden R
import Definition.LogicalRelation.Hidden.Restricted R as R
open import Definition.LogicalRelation.Irrelevance R
open import Definition.LogicalRelation.Properties R
open import Definition.LogicalRelation.ShapeView R
open import Definition.LogicalRelation.Substitution R
open import
  Definition.LogicalRelation.Substitution.Introductions.Universe R
open import Definition.LogicalRelation.Unary R

open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Typed.Reasoning.Reduction R
import Definition.Typed.Stability R as S
open import Definition.Typed.Substitution R
open import Definition.Typed.Well-formed R

open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Properties M

open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Product as Ξ£
import Tools.PropositionalEquality as PE
import Tools.Reasoning.PropositionalEquality

private variable
  Ξ“ Ξ”                               : Con Term _
  A A₁ Aβ‚‚ B t t₁ tβ‚‚ u u₁ uβ‚‚ v v₁ vβ‚‚ : Term _
  σ₁ Οƒβ‚‚                             : Subst _ _
  l lβ€² lβ€³ l‴                        : Universe-level
  p q r                             : M

------------------------------------------------------------------------
-- Characterisation lemmas

opaque

  -- A characterisation lemma for _⊩⟨_⟩_.

  βŠ©β„•β‡” : Ξ“ ⊩⟨ l ⟩ β„• ⇔ ⊒ Ξ“
  βŠ©β„•β‡” =
      (Ξ» βŠ©β„• β†’
        case β„•-view βŠ©β„• of Ξ» {
          (β„•α΅£ β„•β‡’*β„•) β†’
        wfEq (subset* β„•β‡’*β„•) })
    , (Ξ» βŠ’Ξ“ β†’ β„•α΅£ (id (β„•β±Ό βŠ’Ξ“)))

opaque

  -- A characterisation lemma for _⊩⟨_⟩_∷_.

  βŠ©β„•βˆ·U⇔ : Ξ“ ⊩⟨ 1 ⟩ β„• ∷ U 0 ⇔ ⊒ Ξ“
  βŠ©β„•βˆ·U⇔ =
      (Ξ» βŠ©β„• β†’
         case ⊩∷U⇔ .proj₁ βŠ©β„• of Ξ»
           (_ , _ , _ , β„•β‡’* , _) β†’
         wfEqTerm (subset*Term β„•β‡’*))
    , (Ξ» βŠ’Ξ“ β†’
         ⊩∷U⇔ .projβ‚‚
           ( β‰€α΅˜-refl , βŠ©β„•β‡” .projβ‚‚ βŠ’Ξ“
           , (_ , id (β„•β±Ό βŠ’Ξ“) , β„•β‚™ , β‰…β‚œ-β„•refl βŠ’Ξ“)
           ))

opaque
  unfolding _⊩⟨_⟩_≑_

  -- A characterisation lemma for _⊩⟨_⟩_≑_.

  βŠ©β„•β‰‘β‡” : Ξ“ ⊩⟨ l ⟩ β„• ≑ A ⇔ Ξ“ βŠ©β„• β„• ≑ A
  βŠ©β„•β‰‘β‡” =
      (Ξ» (βŠ©β„• , _ , ℕ≑A) β†’
         case β„•-view βŠ©β„• of Ξ» {
           (β„•α΅£ _) β†’
         ℕ≑A })
    , (Ξ» ℕ≑A β†’
         case id (β„•β±Ό (wfEq (subset* ℕ≑A))) of Ξ»
           β„•β‡’*β„• β†’
         let βŠ©β„• = β„•α΅£ β„•β‡’*β„• in
           βŠ©β„•
         , (redSubst* ℕ≑A βŠ©β„•) .proj₁
         , ℕ≑A)

opaque

  -- A characterisation lemma for _⊩⟨_⟩_≑_∷_.

  βŠ©β„•β‰‘β„•βˆ·U⇔ : Ξ“ ⊩⟨ 1 ⟩ β„• ≑ β„• ∷ U 0 ⇔ ⊒ Ξ“
  βŠ©β„•β‰‘β„•βˆ·U⇔ =
      (Ξ» ℕ≑ℕ β†’
         case βŠ©β‰‘βˆ·U⇔ .proj₁ ℕ≑ℕ of Ξ»
           (_ , _ , _ , _ , β„•β‡’* , _) β†’
         wfEqTerm (subset*Term β„•β‡’*))
    , (Ξ» βŠ’Ξ“ β†’
         case id (β„•β±Ό βŠ’Ξ“) of Ξ»
           β„•β‡’*β„• β†’
         βŠ©β‰‘βˆ·U⇔ .projβ‚‚
           ( β‰€α΅˜-refl , βŠ©β„•β‰‘β‡” .projβ‚‚ (id (β„•β±Ό βŠ’Ξ“))
           , (_ , _ , β„•β‡’*β„• , β„•β‡’*β„• , β„•β‚™ , β„•β‚™ , β‰…β‚œ-β„•refl βŠ’Ξ“)
           ))

opaque
  unfolding _⊩⟨_⟩_≑_∷_

  -- A characterisation lemma for _⊩⟨_⟩_≑_∷_.

  βŠ©β‰‘βˆ·β„•β‡” : Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ β„• ⇔ Ξ“ βŠ©β„• t ≑ u βˆ·β„•
  βŠ©β‰‘βˆ·β„•β‡” =
      (Ξ» (βŠ©β„• , t≑u) β†’
         case β„•-view βŠ©β„• of Ξ» {
           (β„•α΅£ _) β†’
         t≑u })
    , (Ξ» t≑u β†’
         β„•α΅£ (id (β„•β±Ό (wfEqTerm (subset*Term (_βŠ©β„•_≑_βˆ·β„•.d t≑u))))) , t≑u)

opaque

  -- A characterisation lemma for _⊩⟨_⟩_∷_.

  βŠ©βˆ·β„•β‡” : Ξ“ ⊩⟨ l ⟩ t ∷ β„• ⇔ Ξ“ βŠ©β„• t βˆ·β„•
  βŠ©βˆ·β„•β‡” {Ξ“} {l} {t} =
    Ξ“ ⊩⟨ l ⟩ t ∷ β„•      β‡”βŸ¨ βŠ©βˆ·β‡”βŠ©β‰‘βˆ· ⟩
    Ξ“ ⊩⟨ l ⟩ t ≑ t ∷ β„•  β‡”βŸ¨ βŠ©β‰‘βˆ·β„•β‡” ⟩
    Ξ“ βŠ©β„• t ≑ t βˆ·β„•       β‡”Λ˜βŸ¨ βŠ©β„•βˆ·β„•β‡”βŠ©β„•β‰‘βˆ·β„• ⟩
    Ξ“ βŠ©β„• t βˆ·β„•           ░⇔

opaque

  -- A characterisation lemma for _⊩⟨_⟩_∷_.

  ⊩zeroβˆ·β„•β‡” : Ξ“ ⊩⟨ l ⟩ zero ∷ β„• ⇔ ⊒ Ξ“
  ⊩zeroβˆ·β„•β‡” =
      wfTerm βˆ˜β†’ escape-⊩∷
    , (Ξ» βŠ’Ξ“ β†’
         βŠ©βˆ·β„•β‡” .projβ‚‚ $
         β„•β‚œ _ (id (zeroβ±Ό βŠ’Ξ“)) (β‰…β‚œ-zerorefl βŠ’Ξ“) zeroα΅£)

opaque

  -- A characterisation lemma for _⊩⟨_⟩_≑_∷_.

  ⊩zero≑zeroβˆ·β„•β‡” : Ξ“ ⊩⟨ l ⟩ zero ≑ zero ∷ β„• ⇔ ⊒ Ξ“
  ⊩zero≑zeroβˆ·β„•β‡” {Ξ“} {l} =
    Ξ“ ⊩⟨ l ⟩ zero ≑ zero ∷ β„•  β‡”Λ˜βŸ¨ βŠ©βˆ·β‡”βŠ©β‰‘βˆ· ⟩
    Ξ“ ⊩⟨ l ⟩ zero ∷ β„•         β‡”βŸ¨ ⊩zeroβˆ·β„•β‡” ⟩
    ⊒ Ξ“                       ░⇔

opaque

  -- A characterisation lemma for _⊩⟨_⟩_≑_∷_.

  ⊩suc≑sucβˆ·β„•β‡” :
    Ξ“ ⊩⟨ l ⟩ suc t ≑ suc u ∷ β„• ⇔
    Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ β„•
  ⊩suc≑sucβˆ·β„•β‡” {Ξ“} {l} {t} {u} =
    Ξ“ ⊩⟨ l ⟩ suc t ≑ suc u ∷ β„•  β‡”βŸ¨ βŠ©β‰‘βˆ·β„•β‡” ⟩
    Ξ“ βŠ©β„• suc t ≑ suc u βˆ·β„•       β‡”βŸ¨ lemma₁ , lemmaβ‚‚ ⟩
    Ξ“ βŠ©β„• t ≑ u βˆ·β„•               β‡”Λ˜βŸ¨ βŠ©β‰‘βˆ·β„•β‡” ⟩
    Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ β„•          ░⇔
    where
    lemmaβ‚€ : [Natural]-prop Ξ“ (suc t) (suc u) β†’ Ξ“ βŠ©β„• t ≑ u βˆ·β„•
    lemmaβ‚€ (sucα΅£ t≑u)             = t≑u
    lemmaβ‚€ (ne (neNfβ‚œβ‚Œ _ () _ _))

    lemma₁ : Ξ“ βŠ©β„• suc t ≑ suc u βˆ·β„• β†’ Ξ“ βŠ©β„• t ≑ u βˆ·β„•
    lemma₁ (β„•β‚œβ‚Œ _ _ suc-tβ‡’*tβ€² suc-uβ‡’*uβ€² _ t′≑uβ€²) =
      case whnfRed*Term suc-t⇒*t′ sucₙ of λ {
        PE.refl β†’
      case whnfRed*Term suc-u⇒*u′ sucₙ of λ {
        PE.refl β†’
      lemmaβ‚€ t′≑uβ€²}}

    lemmaβ‚‚ : Ξ“ βŠ©β„• t ≑ u βˆ·β„• β†’ Ξ“ βŠ©β„• suc t ≑ suc u βˆ·β„•
    lemmaβ‚‚
      t≑u@(β„•β‚œβ‚Œ _ _ tβ‡’*tβ€² uβ‡’*uβ€² tβ€²β‰…uβ€² t′≑uβ€²) =
      let tβ€²-ok , uβ€²-ok = split t′≑uβ€² in
      β„•β‚œβ‚Œ _ _ (id (sucβ±Ό (redFirst*Term tβ‡’*tβ€²)))
        (id (sucⱼ (redFirst*Term u⇒*u′)))
        (β‰…-suc-cong $
         β‰…β‚œ-red (id (β„•β±Ό (wfEqTerm (β‰…β‚œ-eq tβ€²β‰…uβ€²))) , β„•β‚™)
           (t⇒*t′ , naturalWhnf t′-ok) (u⇒*u′ , naturalWhnf u′-ok)
           tβ€²β‰…uβ€²)
        (sucα΅£ t≑u)

opaque

  -- A characterisation lemma for _⊩⟨_⟩_∷_.

  ⊩sucβˆ·β„•β‡” :
    Ξ“ ⊩⟨ l ⟩ suc t ∷ β„• ⇔
    Ξ“ ⊩⟨ l ⟩ t ∷ β„•
  ⊩sucβˆ·β„•β‡” {Ξ“} {l} {t} =
    Ξ“ ⊩⟨ l ⟩ suc t ∷ β„•          β‡”βŸ¨ βŠ©βˆ·β‡”βŠ©β‰‘βˆ· ⟩
    Ξ“ ⊩⟨ l ⟩ suc t ≑ suc t ∷ β„•  β‡”βŸ¨ ⊩suc≑sucβˆ·β„•β‡” ⟩
    Ξ“ ⊩⟨ l ⟩ t ≑ t ∷ β„•          β‡”Λ˜βŸ¨ βŠ©βˆ·β‡”βŠ©β‰‘βˆ· ⟩
    Ξ“ ⊩⟨ l ⟩ t ∷ β„•              ░⇔

opaque

  -- A characterisation lemma for _⊩⟨_⟩_≑_∷_.

  ⊩zero≑sucβˆ·β„•β‡” : Ξ“ ⊩⟨ l ⟩ zero ≑ suc t ∷ β„• ⇔ βŠ₯
  ⊩zero≑sucβˆ·β„•β‡” =
      (Ξ» zero≑suc β†’
         case βŠ©β‰‘βˆ·β„•β‡” .proj₁ zero≑suc of Ξ» {
           (β„•β‚œβ‚Œ _ _ zeroβ‡’* sucβ‡’* _ rest) β†’
         case whnfRed*Term zero⇒* zeroₙ of λ {
           PE.refl β†’
         case whnfRed*Term suc⇒* sucₙ of λ {
           PE.refl β†’
         case rest of Ξ» where
           (ne (neNfβ‚œβ‚Œ _ () _ _)) }}})
    , βŠ₯-elim

------------------------------------------------------------------------
-- β„•

opaque

  -- Validity of β„•, seen as a type former.

  β„•α΅› : βŠ©α΅› Ξ“ β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ β„•
  β„•α΅› {Ξ“} {l} βŠ©Ξ“ =
    βŠ©α΅›β‡”Κ° .projβ‚‚
      ( βŠ©Ξ“
      , Ξ» {_} {Ξ” = Ξ”} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} β†’
          Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“  β†’βŸ¨ proj₁ βˆ˜β†’ escape-βŠ©Λ’β‰‘βˆ· ⟩
          ⊒ Ξ”               β†’βŸ¨ β„•β±Ό ⟩
          (Ξ” ⊒ β„•)           β†’βŸ¨ id ⟩
          Ξ” ⊒ β„• β‡’* β„•        β‡”Λ˜βŸ¨ βŠ©β„•β‰‘β‡” βŸ©β†’
          Ξ” ⊩⟨ l ⟩ β„• ≑ β„•    β–‘
      )

opaque

  -- Validity of β„•, seen as a term former.

  β„•α΅—α΅› : βŠ©α΅› Ξ“ β†’ Ξ“ βŠ©α΅›βŸ¨ 1 ⟩ β„• ∷ U 0
  β„•α΅—α΅› {Ξ“} βŠ©Ξ“ =
    βŠ©α΅›βˆ·β‡”Κ° .projβ‚‚
      ( βŠ©α΅›U βŠ©Ξ“
      , Ξ» {_} {Ξ” = Ξ”} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} β†’
          Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“      β†’βŸ¨ proj₁ βˆ˜β†’ escape-βŠ©Λ’β‰‘βˆ· ⟩
          ⊒ Ξ”                   β‡”Λ˜βŸ¨ βŠ©β„•β‰‘β„•βˆ·U⇔ βŸ©β†’
          Ξ” ⊩⟨ 1 ⟩ β„• ≑ β„• ∷ U 0  β–‘
      )

------------------------------------------------------------------------
-- The constructors zero and suc

opaque

  -- Reducibility of zero.

  ⊩zero :
    ⊒ Ξ“ β†’
    Ξ“ ⊩⟨ l ⟩ zero ∷ β„•
  ⊩zero = ⊩zeroβˆ·β„•β‡” .projβ‚‚

opaque

  -- Validity of zero.

  zeroα΅› :
    βŠ©α΅› Ξ“ β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ zero ∷ β„•
  zeroα΅› {Ξ“} {l} βŠ©Ξ“ =
    βŠ©α΅›βˆ·β‡”Κ° .projβ‚‚
      ( β„•α΅› βŠ©Ξ“
      , Ξ» {_} {Ξ” = Ξ”} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} β†’
          Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“          β†’βŸ¨ proj₁ βˆ˜β†’ escape-βŠ©Λ’β‰‘βˆ· ⟩
          ⊒ Ξ”                       β‡”Λ˜βŸ¨ ⊩zero≑zeroβˆ·β„•β‡” βŸ©β†’
          Ξ” ⊩⟨ l ⟩ zero ≑ zero ∷ β„•  β–‘
      )

opaque

  -- Reducibility of suc.

  ⊩suc :
    Ξ“ ⊩⟨ l ⟩ t ∷ β„• β†’
    Ξ“ ⊩⟨ l ⟩ suc t ∷ β„•
  ⊩suc = ⊩sucβˆ·β„•β‡” .projβ‚‚

opaque

  -- Reducibility of equality between applications of suc.

  ⊩suc≑suc :
    Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ β„• β†’
    Ξ“ ⊩⟨ l ⟩ suc t ≑ suc u ∷ β„•
  ⊩suc≑suc = ⊩suc≑sucβˆ·β„•β‡” .projβ‚‚

opaque

  -- Validity of equality preservation for suc.

  suc-congα΅› :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ β„• β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ suc t ≑ suc u ∷ β„•
  suc-congα΅› t≑u =
    βŠ©α΅›β‰‘βˆ·β‡”Κ° .projβ‚‚
      ( β„•α΅› (wf-βŠ©α΅› $ wf-βŠ©α΅›βˆ· $ wf-βŠ©α΅›β‰‘βˆ· t≑u .proj₁)
      , ⊩suc≑suc βˆ˜β†’ R.βŠ©β‰‘βˆ·β†’ βˆ˜β†’ βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]≑[]∷ t≑u
      )

opaque

  -- Validity of suc.

  sucα΅› :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ β„• β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ suc t ∷ β„•
  sucα΅› ⊩t =
    βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ $
    suc-congα΅› (refl-βŠ©α΅›β‰‘βˆ· ⊩t)

------------------------------------------------------------------------
-- The eliminator natrec

private opaque

  -- A lemma used to prove ⊩natrec≑natrec.

  ⊩natrec≑natrecβ€² :
    Ξ“ βˆ™ β„• ⊒ A₁ β‰… Aβ‚‚ β†’
    (βˆ€ {v₁ vβ‚‚} β†’
     Ξ“ ⊩⟨ l ⟩ v₁ ≑ vβ‚‚ ∷ β„• β†’
     Ξ“ ⊩⟨ l ⟩ A₁ [ v₁ ]β‚€ ≑ A₁ [ vβ‚‚ ]β‚€) β†’
    (βˆ€ {v₁ vβ‚‚} β†’
     Ξ“ ⊩⟨ l ⟩ v₁ ≑ vβ‚‚ ∷ β„• β†’
     Ξ“ ⊩⟨ l ⟩ Aβ‚‚ [ v₁ ]β‚€ ≑ Aβ‚‚ [ vβ‚‚ ]β‚€) β†’
    (βˆ€ {v₁ vβ‚‚} β†’
     Ξ“ ⊩⟨ l ⟩ v₁ ≑ vβ‚‚ ∷ β„• β†’
     Ξ“ ⊩⟨ l ⟩ A₁ [ v₁ ]β‚€ ≑ Aβ‚‚ [ vβ‚‚ ]β‚€) β†’
    Ξ“ ⊒ t₁ ∷ A₁ [ zero ]β‚€ β†’
    Ξ“ ⊒ tβ‚‚ ∷ Aβ‚‚ [ zero ]β‚€ β†’
    Ξ“ ⊩⟨ l ⟩ t₁ ≑ tβ‚‚ ∷ A₁ [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A₁ ⊒ u₁ β‰… uβ‚‚ ∷ A₁ [ suc (var x1) ]↑² β†’
    (βˆ€ {v₁ vβ‚‚ w₁ wβ‚‚} β†’
     Ξ“ ⊩⟨ l ⟩ v₁ ≑ vβ‚‚ ∷ β„• β†’
     Ξ“ ⊩⟨ l ⟩ w₁ ≑ wβ‚‚ ∷ A₁ [ v₁ ]β‚€ β†’
     Ξ“ ⊩⟨ l ⟩ u₁ [ v₁ , w₁ ]₁₀ ≑ uβ‚‚ [ vβ‚‚ , wβ‚‚ ]₁₀ ∷ A₁ [ suc v₁ ]β‚€) β†’
    Ξ“ βŠ©β„• v₁ ≑ vβ‚‚ βˆ·β„• β†’
    Ξ“ ⊩⟨ l ⟩ natrec p q r A₁ t₁ u₁ v₁ ≑
      natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ vβ‚‚ ∷ A₁ [ v₁ ]β‚€
  ⊩natrec≑natrecβ€²
    {A₁} {Aβ‚‚} {l} {t₁} {tβ‚‚} {u₁} {uβ‚‚} {v₁} {vβ‚‚} {p} {q} {r}
    A₁≅Aβ‚‚ A₁≑A₁ A₂≑Aβ‚‚ A₁≑Aβ‚‚ ⊒t₁ ⊒tβ‚‚ t₁≑tβ‚‚ u₁≅uβ‚‚ u₁≑uβ‚‚
    βŠ©β„•-v₁≑vβ‚‚@(β„•β‚œβ‚Œ v₁′ vβ‚‚β€² v₁⇒*v₁′ vβ‚‚β‡’*vβ‚‚β€² v₁′≅vβ‚‚β€² vβ‚β€²βˆΌvβ‚‚β€²) =
    let ⊒A₁≑Aβ‚‚        = β‰…-eq A₁≅Aβ‚‚
        _ , ⊒u₁ , ⊒uβ‚‚ = wf-βŠ’β‰‘βˆ· (β‰…β‚œ-eq u₁≅uβ‚‚)
        ⊒uβ‚‚           =
          S.stabilityTerm (S.refl-βˆ™ ⊒A₁≑Aβ‚‚)
            (conv ⊒uβ‚‚ $
             subst-βŠ’β‰‘ ⊒A₁≑Aβ‚‚ $ refl-βŠ’Λ’Κ·β‰‘βˆ· $
             ⊒˒ʷ∷-[][]↑ (sucβ±Ό (var₁ (wf-βŠ’β‰‘ ⊒A₁≑Aβ‚‚ .proj₁))))
    in

    -- Some definitions related to v₁ andΒ vβ‚‚.
    case βŠ©β‰‘βˆ·β„•β‡” {l = l} .projβ‚‚ βŠ©β„•-v₁≑vβ‚‚ of Ξ»
      v₁≑vβ‚‚ β†’
    case wf-βŠ©β‰‘βˆ· v₁≑vβ‚‚ of Ξ»
      (⊩v₁ , ⊩vβ‚‚) β†’

    -- Some definitions related to v₁′ andΒ vβ‚‚β€².
    case ⊩∷-β‡’* v₁⇒*v₁′ ⊩v₁ of Ξ»
      v₁≑v₁′ β†’
    case ⊩∷-β‡’* vβ‚‚β‡’*vβ‚‚β€² ⊩vβ‚‚ of Ξ»
      v₂≑vβ‚‚β€² β†’
    case
      v₁′  β‰‘Λ˜βŸ¨ v₁≑v₁′ ⟩⊩∷
      v₁   β‰‘βŸ¨ v₁≑vβ‚‚ ⟩⊩∷
      vβ‚‚   β‰‘βŸ¨ v₂≑vβ‚‚β€² ⟩⊩∷∎
      vβ‚‚β€²  ∎
    of Ξ»
      v₁′≑vβ‚‚β€² β†’
    case A₁≑Aβ‚‚ v₁′≑vβ‚‚β€² of Ξ»
      A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] β†’
    case β‰…-eq $ escape-βŠ©β‰‘ A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] of Ξ»
      ⊒A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] β†’

    -- The two applications of natrec are equal if applications of
    -- natrec to v₁′ and vβ‚‚β€² are equal.
    case
      (Ξ» (hyp : _ ⊩⟨ l ⟩ _ ≑ _ ∷ _) β†’
         natrec p q r A₁ t₁ u₁ v₁ ∷ A₁ [ v₁ ]β‚€    β‡’*⟨ natrec-subst* ⊒t₁ ⊒u₁ v₁⇒*v₁′ ⟩⊩∷∷
                                                    ⟨ A₁≑A₁ v₁≑v₁′ ⟩⊩∷
         natrec p q r A₁ t₁ u₁ v₁′ ∷ A₁ [ v₁′ ]β‚€  β‰‘βŸ¨ hyp βŸ©βŠ©βˆ·βˆ·β‡*
                                                   ⟨ ⊒A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] βŸ©β‡’
                                   ∷ Aβ‚‚ [ vβ‚‚β€² ]β‚€  ˘⟨ β‰…-eq $ escape-βŠ©β‰‘ $ A₂≑Aβ‚‚ v₂≑vβ‚‚β€² βŸ©β‡
         natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ vβ‚‚β€² ∷ Aβ‚‚ [ vβ‚‚ ]β‚€   ⇐*⟨ natrec-subst* ⊒tβ‚‚ ⊒uβ‚‚ vβ‚‚β‡’*vβ‚‚β€² ⟩∎∷
         natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ vβ‚‚                 ∎)
    of Ξ»
      lemma β†’

    lemma
      (case vβ‚β€²βˆΌvβ‚‚β€² of Ξ» where
         -- If v₁′ and vβ‚‚β€² are equal neutral terms, then one can
         -- conclude by using the fact that the applications of natrec
         -- to v₁′ and vβ‚‚β€² are equal neutral terms.
         (ne (neNfβ‚œβ‚Œ inc v₁′-ne vβ‚‚β€²-ne v₁′~vβ‚‚β€²)) β†’
           neutral-βŠ©β‰‘βˆ· inc (wf-βŠ©β‰‘ A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] .proj₁)
             (natrecβ‚™ v₁′-ne) (natrecβ‚™ vβ‚‚β€²-ne) $
           ~-natrec A₁≅Aβ‚‚ (escape-βŠ©β‰‘βˆ· t₁≑tβ‚‚) u₁≅uβ‚‚ v₁′~vβ‚‚β€²

         -- If v₁′ and vβ‚‚β€² are both zero, then one can conclude by
         -- using the rule natrec-zero and the fact that t₁ is equal
         -- toΒ tβ‚‚.
         zeroα΅£ β†’
           natrec p q r A₁ t₁ u₁ zero  β‡’βŸ¨ natrec-zero ⊒t₁ ⊒u₁ ⟩⊩∷
           t₁ ∷ A₁ [ zero ]β‚€           β‰‘βŸ¨ t₁≑tβ‚‚ βŸ©βŠ©βˆ·βˆ·β‡*
                                        ⟨ ⊒A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] βŸ©β‡’
           tβ‚‚ ∷ Aβ‚‚ [ zero ]β‚€           β‡βŸ¨ natrec-zero ⊒tβ‚‚ ⊒uβ‚‚ ⟩∎∷
           natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ zero  ∎

         -- If v₁′ and vβ‚‚β€² are applications of suc to equal terms,
         -- then one can conclude by using the rule natrec-suc and an
         -- inductive hypothesis.
         (sucα΅£ {n = v₁″} {nβ€² = vβ‚‚β€³} βŠ©β„•-v₁″≑vβ‚‚β€³) β†’
           case βŠ©β‰‘βˆ·β„•β‡” .projβ‚‚ βŠ©β„•-v₁″≑vβ‚‚β€³ of Ξ»
             v₁″≑vβ‚‚β€³ β†’
           case wf-βŠ©β‰‘βˆ· v₁″≑vβ‚‚β€³ of Ξ»
             (⊩v₁″ , ⊩vβ‚‚β€³) β†’

           natrec p q r A₁ t₁ u₁ (suc v₁″)                             β‡’βŸ¨ natrec-suc ⊒t₁ ⊒u₁ (escape-⊩∷ ⊩v₁″) ⟩⊩∷
           u₁ [ v₁″ , natrec p q r A₁ t₁ u₁ v₁″ ]₁₀ ∷ A₁ [ suc v₁″ ]β‚€  β‰‘βŸ¨ u₁≑uβ‚‚ v₁″≑vβ‚‚β€³ $
                                                                          ⊩natrec≑natrecβ€² A₁≅Aβ‚‚ A₁≑A₁ A₂≑Aβ‚‚ A₁≑Aβ‚‚ ⊒t₁ ⊒tβ‚‚ t₁≑tβ‚‚
                                                                            u₁≅uβ‚‚ u₁≑uβ‚‚ βŠ©β„•-v₁″≑vβ‚‚β€³ βŸ©βŠ©βˆ·βˆ·β‡*
                                                                        ⟨ ⊒A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] βŸ©β‡’
           uβ‚‚ [ vβ‚‚β€³ , natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ vβ‚‚β€³ ]₁₀ ∷ Aβ‚‚ [ suc vβ‚‚β€³ ]β‚€  β‡βŸ¨ natrec-suc ⊒tβ‚‚ ⊒uβ‚‚ (escape-⊩∷ ⊩vβ‚‚β€³)
                                                                        ⟩∎∷
           natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ (suc vβ‚‚β€³)                             ∎)

opaque

  -- Reducibility of equality between applications of natrec.

  ⊩natrec≑natrec :
    Ξ“ βˆ™ β„• ⊒ A₁ ≑ Aβ‚‚ β†’
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ l ⟩ A₁ ≑ Aβ‚‚ β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t₁ ≑ tβ‚‚ ∷ A₁ [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A₁ ⊒ u₁ ≑ uβ‚‚ ∷ A₁ [ suc (var x1) ]↑² β†’
    Ξ“ βˆ™ β„• βˆ™ A₁ βŠ©α΅›βŸ¨ lβ€³ ⟩ u₁ ≑ uβ‚‚ ∷ A₁ [ suc (var x1) ]↑² β†’
    Ξ“ βŠ©α΅›βŸ¨ l‴ ⟩ v₁ ≑ vβ‚‚ ∷ β„• β†’
    ⦃ inc : Neutrals-included or-empty Ξ” ⦄ β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ natrec p q r A₁ t₁ u₁ v₁ [ σ₁ ] ≑
      natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ vβ‚‚ [ Οƒβ‚‚ ] ∷ A₁ [ v₁ ]β‚€ [ σ₁ ]
  ⊩natrec≑natrec
    {A₁} {Aβ‚‚} {l} {σ₁} ⊒A₁≑Aβ‚‚ A₁≑Aβ‚‚ t₁≑tβ‚‚ ⊒u₁≑uβ‚‚ u₁≑uβ‚‚ v₁≑vβ‚‚ σ₁≑σ₂ =
    case wf-βŠ©α΅›β‰‘ A₁≑Aβ‚‚ of Ξ»
      (⊩A₁ , ⊩Aβ‚‚) β†’
    case wf-βŠ©α΅›β‰‘βˆ· t₁≑tβ‚‚ of Ξ»
      (_ , ⊩tβ‚‚) β†’
    case conv-βŠ©α΅›βˆ·
           (βŠ©α΅›β‰‘β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₀≑[]β‚€ A₁≑Aβ‚‚ $
            refl-βŠ©α΅›β‰‘βˆ· $ zeroα΅› {l = l} $ wf-βŠ©α΅› (wf-βŠ©α΅›βˆ· ⊩tβ‚‚))
           ⊩tβ‚‚ of Ξ»
      ⊩tβ‚‚ β†’
    case wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ of Ξ»
      (βŠ©Οƒβ‚ , βŠ©Οƒβ‚‚) β†’
    case escape-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ of Ξ»
      (_ , βŠ’Οƒβ‚β‰‘Οƒβ‚‚) β†’
    case PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (singleSubstLift A₁ _) $
         R.βŠ©β‰‘βˆ·β†’ $ βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]≑[]∷ t₁≑tβ‚‚ σ₁≑σ₂ of Ξ»
      t₁[σ₁]≑tβ‚‚[Οƒβ‚‚] β†’
    PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (PE.sym $ singleSubstLift A₁ _) $
    ⊩natrec≑natrecβ€²
      (with-inc-βŠ’β‰… (subst-βŠ’β‰‘-⇑ ⊒A₁≑Aβ‚‚ βŠ’Οƒβ‚β‰‘Οƒβ‚‚) $
       R.escape-βŠ©β‰‘ ⦃ inc = included ⦄ (βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑] A₁≑Aβ‚‚ σ₁≑σ₂))
      (R.βŠ©β‰‘β†’ βˆ˜β†’
       βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ (refl-βŠ©α΅›β‰‘ ⊩A₁) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒβ‚) βˆ˜β†’
       R.β†’βŠ©β‰‘βˆ·)
      (R.βŠ©β‰‘β†’ βˆ˜β†’
       βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ (refl-βŠ©α΅›β‰‘ ⊩Aβ‚‚) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒβ‚‚) βˆ˜β†’
       R.β†’βŠ©β‰‘βˆ·)
      (R.βŠ©β‰‘β†’ βˆ˜β†’ βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ A₁≑Aβ‚‚ σ₁≑σ₂ βˆ˜β†’ R.β†’βŠ©β‰‘βˆ·)
      (escape-⊩∷ $ wf-βŠ©β‰‘βˆ· t₁[σ₁]≑tβ‚‚[Οƒβ‚‚] .proj₁)
      (PE.subst (_⊒_∷_ _ _) (singleSubstLift Aβ‚‚ _) $
       R.escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩tβ‚‚ βŠ©Οƒβ‚‚)
      (level-βŠ©β‰‘βˆ·
         (wf-βŠ©β‰‘
            (R.βŠ©β‰‘β†’ $
             βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ A₁≑Aβ‚‚ σ₁≑σ₂ $ R.β†’βŠ©β‰‘βˆ· $
             refl-βŠ©β‰‘βˆ· $ ⊩zero {l = l} $ escape-⊩˒∷ βŠ©Οƒβ‚ .proj₁)
            .proj₁)
         t₁[σ₁]≑tβ‚‚[Οƒβ‚‚])
      (with-inc-βŠ’β‰…βˆ·
         (PE.subst (_⊒_≑_∷_ _ _ _) ([][]↑-commutes A₁) $
          subst-βŠ’β‰‘βˆ·-⇑ ⊒u₁≑uβ‚‚ βŠ’Οƒβ‚β‰‘Οƒβ‚‚)
         (PE.subst (_⊒_β‰…_∷_ _ _ _) (natrecSucCase _ A₁) $
          R.escape-βŠ©β‰‘βˆ· ⦃ inc = included ⦄ $
          βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑]∷ u₁≑uβ‚‚ σ₁≑σ₂))
      (Ξ» {v₁ = v₁} {vβ‚‚ = _} {w₁ = w₁} v₁≑vβ‚‚ w₁≑wβ‚‚ β†’
         level-βŠ©β‰‘βˆ·
           (wf-βŠ©β‰‘
              (R.βŠ©β‰‘β†’ $ βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ A₁≑Aβ‚‚ σ₁≑σ₂ $
               R.β†’βŠ©β‰‘βˆ· $ ⊩suc≑suc v₁≑vβ‚‚)
              .proj₁) $
         PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _)
           (A₁ [ suc (var x1) ]↑² [ σ₁ ⇑ ⇑ ] [ v₁ , w₁ ]₁₀  β‰‘βŸ¨ PE.cong _[ _ , _ ]₁₀ $ natrecSucCase _ A₁ ⟩
            A₁ [ σ₁ ⇑ ] [ suc (var x1) ]↑² [ v₁ , w₁ ]₁₀    β‰‘Λ˜βŸ¨ substComp↑² (A₁ [ _ ]) _ ⟩
            A₁ [ σ₁ ⇑ ] [ suc v₁ ]β‚€                         ∎) $
         R.βŠ©β‰‘βˆ·β†’ $
         βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]β‚β‚€βˆ· u₁≑uβ‚‚ σ₁≑σ₂
           (R.β†’βŠ©β‰‘βˆ· v₁≑vβ‚‚) (R.β†’βŠ©β‰‘βˆ· w₁≑wβ‚‚))
      (βŠ©β‰‘βˆ·β„•β‡” .proj₁ $ R.βŠ©β‰‘βˆ·β†’ $ βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]≑[]∷ v₁≑vβ‚‚ σ₁≑σ₂)
    where
    open Tools.Reasoning.PropositionalEquality

opaque

  -- Validity of equality preservation for natrec.

  natrec-congα΅› :
    Ξ“ βˆ™ β„• ⊒ A₁ ≑ Aβ‚‚ β†’
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ l ⟩ A₁ ≑ Aβ‚‚ β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t₁ ≑ tβ‚‚ ∷ A₁ [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A₁ ⊒ u₁ ≑ uβ‚‚ ∷ A₁ [ suc (var x1) ]↑² β†’
    Ξ“ βˆ™ β„• βˆ™ A₁ βŠ©α΅›βŸ¨ lβ€³ ⟩ u₁ ≑ uβ‚‚ ∷ A₁ [ suc (var x1) ]↑² β†’
    Ξ“ βŠ©α΅›βŸ¨ l‴ ⟩ v₁ ≑ vβ‚‚ ∷ β„• β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ natrec p q r A₁ t₁ u₁ v₁ ≑ natrec p q r Aβ‚‚ tβ‚‚ uβ‚‚ vβ‚‚ ∷
      A₁ [ v₁ ]β‚€
  natrec-congα΅› ⊒A₁≑Aβ‚‚ A₁≑Aβ‚‚ t₁≑tβ‚‚ ⊒u₁≑uβ‚‚ u₁≑uβ‚‚ v₁≑vβ‚‚ =
    βŠ©α΅›β‰‘βˆ·β‡”Κ° .projβ‚‚
      ( βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚€ (wf-βŠ©α΅›β‰‘ A₁≑Aβ‚‚ .proj₁) (wf-βŠ©α΅›β‰‘βˆ· v₁≑vβ‚‚ .proj₁)
      , ⊩natrec≑natrec ⊒A₁≑Aβ‚‚ A₁≑Aβ‚‚ t₁≑tβ‚‚ ⊒u₁≑uβ‚‚ u₁≑uβ‚‚ v₁≑vβ‚‚
      )

opaque

  -- Validity of natrec.

  natrecα΅› :
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ∷ A [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A ⊒ u ∷ A [ suc (var x1) ]↑² β†’
    Ξ“ βˆ™ β„• βˆ™ A βŠ©α΅›βŸ¨ lβ€³ ⟩ u ∷ A [ suc (var x1) ]↑² β†’
    Ξ“ βŠ©α΅›βŸ¨ l‴ ⟩ v ∷ β„• β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ natrec p q r A t u v ∷ A [ v ]β‚€
  natrecα΅› ⊩A ⊩t ⊒u ⊩u ⊩v =
    βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ $
    natrec-congα΅› (refl (βŠ’βˆ™β†’βŠ’ (wfTerm ⊒u))) (refl-βŠ©α΅›β‰‘ ⊩A) (refl-βŠ©α΅›β‰‘βˆ· ⊩t)
      (refl ⊒u) (refl-βŠ©α΅›β‰‘βˆ· ⊩u) (refl-βŠ©α΅›β‰‘βˆ· ⊩v)

opaque

  -- Validity of the equality rule called natrec-zero.

  natrec-zeroα΅› :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A ⊒ u ∷ A [ suc (var x1) ]↑² β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ natrec p q r A t u zero ≑ t ∷ A [ zero ]β‚€
  natrec-zeroα΅› {A} ⊩t ⊒u =
    βŠ©α΅›βˆ·-⇐
      (Ξ» βŠ©Οƒ β†’
         PE.subst (_⊒_β‡’_∷_ _ _ _) (PE.sym $ singleSubstLift A _) $
         natrec-zero
           (PE.subst (_⊒_∷_ _ _) (singleSubstLift A _) $
            R.escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩t βŠ©Οƒ)
           (PE.subst (_⊒_∷_ _ _) (natrecSucCase _ A) $
            subst-⊒∷-⇑ ⊒u (escape-⊩˒∷ βŠ©Οƒ .projβ‚‚)))
      ⊩t

opaque

  -- Validity of the equality rule called natrec-suc.

  natrec-sucα΅› :
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ lβ€² ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€³ ⟩ t ∷ A [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A ⊒ u ∷ A [ suc (var x1) ]↑² β†’
    Ξ“ βˆ™ β„• βˆ™ A βŠ©α΅›βŸ¨ l ⟩ u ∷ A [ suc (var x1) ]↑² β†’
    Ξ“ βŠ©α΅›βŸ¨ l‴ ⟩ v ∷ β„• β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ natrec p q r A t u (suc v) ≑
      u [ v , natrec p q r A t u v ]₁₀ ∷ A [ suc v ]β‚€
  natrec-sucα΅› {A} {u} ⊩A ⊩t ⊒u ⊩u ⊩v =
    βŠ©α΅›βˆ·-⇐
      (Ξ» βŠ©Οƒ β†’
         PE.substβ‚‚ (_⊒_β‡’_∷_ _ _) (PE.sym $ [,]-[]-commute u)
           (PE.sym $ singleSubstLift A _) $
         natrec-suc
           (PE.subst (_⊒_∷_ _ _) (singleSubstLift A _) $
            R.escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩t βŠ©Οƒ)
           (PE.subst (_⊒_∷_ _ _) (natrecSucCase _ A) $
            subst-⊒∷-⇑ ⊒u (escape-⊩˒∷ βŠ©Οƒ .projβ‚‚))
           (R.escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩v βŠ©Οƒ))
      (PE.subst (_βŠ©α΅›βŸ¨_⟩_∷_ _ _ _) (PE.sym $ substComp↑² A _) $
       βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚β‚€βˆ· ⊩u ⊩v (natrecα΅› ⊩A ⊩t ⊒u ⊩u ⊩v))