------------------------------------------------------------------------
-- 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
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.Substitution.Introductions.Var R

open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Typed.Reasoning.Reduction.Primitive 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‴                        : TypeLevel
  p q r                             : M

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

opaque

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

  βŠ©β„•β‡” : Ξ“ ⊩⟨ l ⟩ β„• ⇔ ⊒ Ξ“
  βŠ©β„•β‡” =
      lemma βˆ˜β†’ β„•-elim
    , (Ξ» βŠ’Ξ“ β†’ β„•α΅£ ([_,_,_] (β„•β±Ό βŠ’Ξ“) (β„•β±Ό βŠ’Ξ“) (id (β„•β±Ό βŠ’Ξ“))))
    where
    lemma : Ξ“ ⊩⟨ l βŸ©β„• β„• β†’ ⊒ Ξ“
    lemma (emb 0<1 βŠ©β„•)           = lemma βŠ©β„•
    lemma (noemb [ βŠ’β„• , _ , _ ]) = wf βŠ’β„•

opaque

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

  βŠ©β„•βˆ·U⇔ : Ξ“ ⊩⟨ ΒΉ ⟩ β„• ∷ U ⇔ ⊒ Ξ“
  βŠ©β„•βˆ·U⇔ =
      (Ξ» βŠ©β„• β†’
         case ⊩∷U⇔ .proj₁ βŠ©β„• of Ξ»
           (_ , _ , β„•β‡’* , _) β†’
         wfTerm (⊒t-redβ‚œ β„•β‡’*))
    , (Ξ» βŠ’Ξ“ β†’
         ⊩∷U⇔ .projβ‚‚
           ( (_ , 0<1 , βŠ©β„•β‡” .projβ‚‚ βŠ’Ξ“)
           , (_ , idRedTerm:*: (β„•β±Ό βŠ’Ξ“) , β„•β‚™ , β‰…β‚œ-β„•refl βŠ’Ξ“)
           ))

opaque
  unfolding _⊩⟨_⟩_∷_

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

  βŠ©βˆ·β„•β‡” : Ξ“ ⊩⟨ l ⟩ t ∷ β„• ⇔ Ξ“ βŠ©β„• t βˆ·β„•
  βŠ©βˆ·β„•β‡” =
      (Ξ» (βŠ©β„• , ⊩t) β†’
         lemma (β„•-elim βŠ©β„•)
           ((irrelevanceTerm βŠ©β„•) (β„•-intr (β„•-elim βŠ©β„•)) ⊩t))
    , (Ξ» ⊩t β†’
         β„•α΅£ (idRed:*: (β„•β±Ό (wfTerm (⊒t-redβ‚œ (_βŠ©β„•_βˆ·β„•.d ⊩t))))) , ⊩t)
    where
    lemma :
      (⊩A : Ξ“ ⊩⟨ l βŸ©β„• A) β†’
      Ξ“ ⊩⟨ l ⟩ t ∷ A / β„•-intr ⊩A β†’
      Ξ“ βŠ©β„• t βˆ·β„•
    lemma (noemb _)    ⊩t = ⊩t
    lemma (emb 0<1 ⊩A) ⊩t = lemma ⊩A ⊩t

opaque

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

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

opaque

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

  ⊩sucβˆ·β„•β‡” :
    Ξ“ ⊩⟨ l ⟩ suc t ∷ β„• ⇔
    Ξ“ ⊩⟨ l ⟩ t ∷ β„•
  ⊩sucβˆ·β„•β‡” {Ξ“} {l} {t} =
    Ξ“ ⊩⟨ l ⟩ suc t ∷ β„•  β‡”βŸ¨ βŠ©βˆ·β„•β‡” ⟩
    Ξ“ βŠ©β„• suc t βˆ·β„•       β‡”βŸ¨ (Ξ» (β„•β‚œ _ suc-tβ‡’*u _ u-ok) β†’
                              case whnfRed*Term (redβ‚œ suc-tβ‡’*u) sucβ‚™ of Ξ» {
                                PE.refl β†’
                              lemma u-ok })
                         , (Ξ» ⊩t@(β„•β‚œ _ [ ⊒t , _ , tβ‡’*u ] uβ‰…u u-ok) β†’
                              let tβ†˜u = tβ‡’*u , naturalWhnf (natural u-ok) in
                              β„•β‚œ _ (idRedTerm:*: (sucβ±Ό ⊒t))
                                (β‰…-suc-cong $
                                 β‰…β‚œ-red (id (β„•β±Ό (wfTerm ⊒t)) , β„•β‚™) tβ†˜u tβ†˜u uβ‰…u)
                                (sucᡣ ⊩t))
                         ⟩
    Ξ“ βŠ©β„• t βˆ·β„•           β‡”Λ˜βŸ¨ βŠ©βˆ·β„•β‡” ⟩
    Ξ“ ⊩⟨ l ⟩ t ∷ β„•      ░⇔
    where
    lemma : Natural-prop Ξ“ (suc t) β†’ Ξ“ βŠ©β„• t βˆ·β„•
    lemma (sucᡣ ⊩t) = ⊩t

opaque
  unfolding _⊩⟨_⟩_≑_

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

  βŠ©β„•β‰‘β‡” : Ξ“ ⊩⟨ l ⟩ β„• ≑ A ⇔ Ξ“ βŠ©β„• β„• ≑ A
  βŠ©β„•β‰‘β‡” =
      (Ξ» (βŠ©β„• , _ , ℕ≑A) β†’
         lemma (β„•-elim βŠ©β„•)
           ((irrelevanceEq βŠ©β„•) (β„•-intr (β„•-elim βŠ©β„•)) ℕ≑A))
    , (Ξ» ℕ≑A β†’
         case idRed:*: (β„•β±Ό (wfEq (subset* ℕ≑A))) of Ξ»
           β„•β‡’*β„• β†’
         let βŠ©β„• = β„•α΅£ β„•β‡’*β„• in
           βŠ©β„•
         , (redSubst* ℕ≑A βŠ©β„•) .proj₁
         , ℕ≑A)
    where
    lemma :
      (⊩A : Ξ“ ⊩⟨ l βŸ©β„• A) β†’
      Ξ“ ⊩⟨ l ⟩ A ≑ B / β„•-intr ⊩A β†’
      Ξ“ βŠ©β„• A ≑ B
    lemma (noemb _)    A≑B = A≑B
    lemma (emb 0<1 ⊩A) A≑B = lemma ⊩A A≑B

opaque

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

  βŠ©β„•β‰‘β„•βˆ·U⇔ : Ξ“ ⊩⟨ ΒΉ ⟩ β„• ≑ β„• ∷ U ⇔ ⊒ Ξ“
  βŠ©β„•β‰‘β„•βˆ·U⇔ =
      (Ξ» ℕ≑ℕ β†’
         case βŠ©β‰‘βˆ·U⇔ .proj₁ ℕ≑ℕ of Ξ»
           (_ , _ , _ , β„•β‡’* , _) β†’
         wfTerm (⊒t-redβ‚œ β„•β‡’*))
    , (Ξ» βŠ’Ξ“ β†’
         case idRedTerm:*: (β„•β±Ό βŠ’Ξ“) of Ξ»
           β„•β‡’*β„• β†’
         βŠ©β‰‘βˆ·U⇔ .projβ‚‚
           ( (_ , 0<1 , βŠ©β„•β‰‘β‡” .projβ‚‚ (id (β„•β±Ό βŠ’Ξ“)))
           , (_ , _ , β„•β‡’*β„• , β„•β‡’*β„• , β„•β‚™ , β„•β‚™ , β‰…β‚œ-β„•refl βŠ’Ξ“)
           ))

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

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

  βŠ©β‰‘βˆ·β„•β‡” :
    Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ β„• ⇔
    (Ξ“ βŠ©β„• t βˆ·β„• Γ— Ξ“ βŠ©β„• u βˆ·β„• Γ— Ξ“ βŠ©β„• t ≑ u βˆ·β„•)
  βŠ©β‰‘βˆ·β„•β‡” =
      (Ξ» (βŠ©β„• , ⊩t , ⊩u , t≑u) β†’
         lemma (β„•-elim βŠ©β„•)
           ((irrelevanceTerm βŠ©β„•) (β„•-intr (β„•-elim βŠ©β„•)) ⊩t)
           ((irrelevanceTerm βŠ©β„•) (β„•-intr (β„•-elim βŠ©β„•)) ⊩u)
           ((irrelevanceEqTerm βŠ©β„•) (β„•-intr (β„•-elim βŠ©β„•)) t≑u))
    , (Ξ» (⊩t , ⊩u , t≑u) β†’
         β„•α΅£ (idRed:*: (β„•β±Ό (wfTerm (⊒t-redβ‚œ (_βŠ©β„•_≑_βˆ·β„•.d t≑u)))))
       , ⊩t , ⊩u , t≑u)
    where
    lemma :
      (⊩A : Ξ“ ⊩⟨ l βŸ©β„• A) β†’
      Ξ“ ⊩⟨ l ⟩ t ∷ A / β„•-intr ⊩A β†’
      Ξ“ ⊩⟨ l ⟩ u ∷ A / β„•-intr ⊩A β†’
      Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ A / β„•-intr ⊩A β†’
      Ξ“ βŠ©β„• t βˆ·β„• Γ— Ξ“ βŠ©β„• u βˆ·β„• Γ— Ξ“ βŠ©β„• t ≑ u βˆ·β„•
    lemma (noemb _)    ⊩t ⊩u t≑u = ⊩t , ⊩u , t≑u
    lemma (emb 0<1 ⊩A) ⊩t ⊩u t≑u = lemma ⊩A ⊩t ⊩u t≑u

opaque

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

  ⊩zero≑zeroβˆ·β„•β‡” : Ξ“ ⊩⟨ l ⟩ zero ≑ zero ∷ β„• ⇔ ⊒ Ξ“
  ⊩zero≑zeroβˆ·β„•β‡” {Ξ“} {l} =
    Ξ“ ⊩⟨ l ⟩ zero ≑ zero ∷ β„•  β‡”βŸ¨ proj₁ βˆ˜β†’ wf-βŠ©β‰‘βˆ· , refl-βŠ©β‰‘βˆ· ⟩
    Ξ“ ⊩⟨ 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 βˆ·β„• Γ— Ξ“ βŠ©β„• suc t ≑ suc u βˆ·β„•  β‡”βŸ¨ βŠ©βˆ·β„•β‡” {l = l} βˆ˜β‡” ⊩sucβˆ·β„•β‡” βˆ˜β‡” sym⇔ βŠ©βˆ·β„•β‡”
                                                                Γ—-cong-⇔
                                                              βŠ©βˆ·β„•β‡” {l = l} βˆ˜β‡” ⊩sucβˆ·β„•β‡” βˆ˜β‡” sym⇔ βŠ©βˆ·β„•β‡”
                                                                Γ—-cong-⇔
                                                              (lemma₁ , lemmaβ‚‚) ⟩
    Ξ“ βŠ©β„• t βˆ·β„• Γ— Ξ“ βŠ©β„• u βˆ·β„• Γ— Ξ“ βŠ©β„• t ≑ u βˆ·β„•                  β‡”Λ˜βŸ¨ βŠ©β‰‘βˆ·β„•β‡” ⟩
    Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ β„•                                     ░⇔
    where
    lemmaβ‚€ : [Natural]-prop Ξ“ (suc t) (suc u) β†’ Ξ“ βŠ©β„• t ≑ u βˆ·β„•
    lemmaβ‚€ (sucα΅£ t≑u) = t≑u

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

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

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 (redβ‚œ zeroβ‡’*) zeroβ‚™ of Ξ» {
           PE.refl β†’
         case whnfRed*Term (redβ‚œ 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.

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

------------------------------------------------------------------------
-- 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 βˆ˜β†’ βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚
      )

opaque

  -- Validity of suc.

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

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

private opaque

  -- A variant of natrec-subst for _⊒_β‡’*_∷_.

  natrec-subst*β€² :
    Ξ“ βˆ™ β„• ⊒ A β†’
    (βˆ€ {v₁ vβ‚‚} β†’
     Ξ“ ⊩⟨ lβ€² ⟩ v₁ ≑ vβ‚‚ ∷ β„• β†’
     Ξ“ ⊩⟨ l ⟩ A [ v₁ ]β‚€ ≑ A [ vβ‚‚ ]β‚€) β†’
    Ξ“ ⊒ t ∷ A [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A ⊒ u ∷ A [ suc (var x1) ]↑² β†’
    Ξ“ ⊒ v₁ β‡’* vβ‚‚ ∷ β„• β†’
    Ξ“ ⊩⟨ lβ€² ⟩ vβ‚‚ ∷ β„• β†’
    Ξ“ ⊒ natrec p q r A t u v₁ β‡’* natrec p q r A t u vβ‚‚ ∷ A [ v₁ ]β‚€
  natrec-subst*β€²
    {A} {t} {u} {v₁} {vβ‚‚} {p} {q} {r} ⊒A A≑A ⊒t ⊒u v₁⇒*vβ‚‚ ⊩vβ‚‚ =
    case v₁⇒*vβ‚‚ of Ξ» where
      (id ⊒v₁) β†’
        id (natrecβ±Ό ⊒A ⊒t ⊒u ⊒v₁)
      (_⇨_ {tβ€² = v₃} v₁⇒v₃ v₃⇒*vβ‚‚) β†’
        case
          v₁  β‡’βŸ¨ v₁⇒v₃ ⟩⊩∷
          v₃  ∎⟨ wf-βŠ©β‰‘βˆ· (⊩∷-⇐* v₃⇒*vβ‚‚ ⊩vβ‚‚) .proj₁ ⟩⊩∷
        of Ξ»
          v₁≑v₃ β†’
        natrec p q r A t u v₁ ∷ A [ v₁ ]β‚€  β‡’βŸ¨ natrec-subst ⊒A ⊒t ⊒u v₁⇒v₃ ⟩∷
                                            ⟨ β‰…-eq $ escape-βŠ©β‰‘ $ A≑A v₁≑v₃ βŸ©β‡’
        natrec p q r A t u v₃ ∷ A [ v₃ ]β‚€  β‡’*⟨ natrec-subst*β€² ⊒A A≑A ⊒t ⊒u v₃⇒*vβ‚‚ ⊩vβ‚‚ ⟩∎∷
        natrec p q r A t u vβ‚‚              ∎

opaque

  -- A variant of natrec-subst for _⊒_β‡’*_∷_.

  natrec-subst* :
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ“ ⊒ t ∷ A [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ A ⊒ u ∷ A [ suc (var x1) ]↑² β†’
    Ξ“ ⊒ v₁ β‡’* vβ‚‚ ∷ β„• β†’
    Ξ“ ⊩⟨ lβ€² ⟩ vβ‚‚ ∷ β„• β†’
    Ξ“ ⊒ natrec p q r A t u v₁ β‡’* natrec p q r A t u vβ‚‚ ∷ A [ v₁ ]β‚€
  natrec-subst* ⊩A =
    natrec-subst*β€² (escape-βŠ©α΅› ⊩A) (βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©[]₀≑[]β‚€ (refl-βŠ©α΅›β‰‘ ⊩A))

private opaque

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

  ⊩natrec≑natrecβ€² :
    Ξ“ βˆ™ β„• ⊒ A₁ β†’
    Ξ“ βˆ™ β„• ⊒ Aβ‚‚ β†’
    Ξ“ βˆ™ β„• ⊒ 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₁ ∷ A₁ [ suc (var x1) ]↑² β†’
    Ξ“ βˆ™ β„• βˆ™ Aβ‚‚ ⊒ uβ‚‚ ∷ Aβ‚‚ [ suc (var x1) ]↑² β†’
    Ξ“ βˆ™ β„• βˆ™ 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β‚‚ βˆ·β„• β†’
    Ξ“ βŠ©β„• 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β‚‚ A₁≑Aβ‚‚ ⊒t₁ ⊒tβ‚‚ t₁≑tβ‚‚ ⊒u₁ ⊒uβ‚‚ u₁≅uβ‚‚ u₁≑uβ‚‚
    βŠ©β„•-v₁@(β„•β‚œ v₁′′ v₁⇒*v₁′′ _ v₁′′-prop)
    βŠ©β„•-vβ‚‚@(β„•β‚œ vβ‚‚β€²β€² vβ‚‚β‡’*vβ‚‚β€²β€² _ vβ‚‚β€²β€²-prop)
    βŠ©β„•-v₁≑vβ‚‚@(β„•β‚œβ‚Œ v₁′ vβ‚‚β€² v₁⇒*v₁′ vβ‚‚β‡’*vβ‚‚β€² v₁′≅vβ‚‚β€² vβ‚β€²βˆΌvβ‚‚β€²) =
    -- The terms v₁′ and v₁′′ are equal, as are the terms vβ‚‚β€²
    -- andΒ vβ‚‚β€²β€².
    case Ξ£.map naturalWhnf naturalWhnf $ split vβ‚β€²βˆΌvβ‚‚β€² of Ξ»
      (v₁′-whnf , vβ‚‚β€²-whnf) β†’
    case whrDet*Term (redβ‚œ v₁⇒*v₁′ , v₁′-whnf)
           (redβ‚œ v₁⇒*v₁′′ , naturalWhnf (natural v₁′′-prop)) of Ξ» {
      PE.refl β†’
    case whrDet*Term (redβ‚œ vβ‚‚β‡’*vβ‚‚β€² , vβ‚‚β€²-whnf)
           (redβ‚œ vβ‚‚β‡’*vβ‚‚β€²β€² , naturalWhnf (natural vβ‚‚β€²β€²-prop)) of Ξ» {
      PE.refl β†’

    -- Some definitions related to v₁ andΒ vβ‚‚.
    case βŠ©β‰‘βˆ·β„•β‡” {l = l} .projβ‚‚ (βŠ©β„•-v₁ , βŠ©β„•-vβ‚‚ , βŠ©β„•-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 wf-βŠ©β‰‘βˆ· v₁≑v₁′ .projβ‚‚ of Ξ»
      ⊩v₁′ β†’
    case wf-βŠ©β‰‘βˆ· v₂≑vβ‚‚β€² .projβ‚‚ of Ξ»
      ⊩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*β€² ⊒A₁ A₁≑A₁ ⊒t₁ ⊒u₁ (redβ‚œ v₁⇒*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*β€² ⊒Aβ‚‚ A₂≑Aβ‚‚ ⊒tβ‚‚ ⊒uβ‚‚ (redβ‚œ vβ‚‚β‡’*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β‚œβ‚Œ v₁′-ne vβ‚‚β€²-ne v₁′~vβ‚‚β€²)) β†’
           neutral-βŠ©β‰‘βˆ· (wf-βŠ©β‰‘ A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] .proj₁)
             (natrecβ‚™ v₁′-ne) (natrecβ‚™ vβ‚‚β€²-ne)
             (natrecβ±Ό ⊒A₁ ⊒t₁ ⊒u₁ (escape-⊩∷ ⊩v₁′))
             (conv (natrecβ±Ό ⊒Aβ‚‚ ⊒tβ‚‚ ⊒uβ‚‚ (escape-⊩∷ ⊩vβ‚‚β€²))
                (sym ⊒A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²])) $
           ~-natrec ⊒A₁ 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 ⊒A₁ ⊒t₁ ⊒u₁ ⟩⊩∷
           t₁ ∷ A₁ [ zero ]β‚€           β‰‘βŸ¨ t₁≑tβ‚‚ βŸ©βŠ©βˆ·βˆ·β‡*
                                        ⟨ ⊒A₁[v₁′]≑Aβ‚‚[vβ‚‚β€²] βŸ©β‡’
           tβ‚‚ ∷ Aβ‚‚ [ zero ]β‚€           β‡βŸ¨ natrec-zero ⊒Aβ‚‚ ⊒tβ‚‚ ⊒uβ‚‚ , ⊒tβ‚‚ ⟩∎∷
           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 v₁′′-prop of Ξ» {
             (ne suc-ne) β†’ case _⊩neNf_∷_.neK suc-ne of Ξ» ();
             (sucα΅£ βŠ©β„•-v₁″) β†’
           case vβ‚‚β€²β€²-prop of Ξ» {
             (ne suc-ne) β†’ case _⊩neNf_∷_.neK suc-ne of Ξ» ();
             (sucα΅£ βŠ©β„•-vβ‚‚β€³) β†’
           case βŠ©β‰‘βˆ·β„•β‡” .projβ‚‚ (βŠ©β„•-v₁″ , βŠ©β„•-vβ‚‚β€³ , βŠ©β„•-v₁″≑vβ‚‚β€³) of Ξ»
             v₁″≑vβ‚‚β€³ β†’
           case wf-βŠ©β‰‘βˆ· v₁″≑vβ‚‚β€³ of Ξ»
             (⊩v₁″ , ⊩vβ‚‚β€³) β†’
           case u₁≑uβ‚‚ v₁″≑vβ‚‚β€³ $
                ⊩natrec≑natrecβ€² ⊒A₁ ⊒Aβ‚‚ A₁≅Aβ‚‚ A₁≑A₁ A₂≑Aβ‚‚ A₁≑Aβ‚‚
                  ⊒t₁ ⊒tβ‚‚ t₁≑tβ‚‚ ⊒u₁ ⊒uβ‚‚ u₁≅uβ‚‚ u₁≑uβ‚‚
                  βŠ©β„•-v₁″ βŠ©β„•-vβ‚‚β€³ βŠ©β„•-v₁″≑vβ‚‚β€³ of Ξ»
             u₁[v₁″,nr]≑uβ‚‚[vβ‚‚β€³,nr] β†’

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

opaque

  -- Reducibility of equality between applications of natrec.

  ⊩natrec≑natrec :
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ l ⟩ A₁ ≑ Aβ‚‚ β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t₁ ≑ tβ‚‚ ∷ A₁ [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ 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≑natrec {l} {A₁} {Aβ‚‚} {σ₁} A₁≑Aβ‚‚ t₁≑tβ‚‚ 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-βŠ©α΅›β‰‘βˆ· u₁≑uβ‚‚ of Ξ»
      (⊩u₁ , ⊩uβ‚‚) β†’
    case conv-βˆ™-βŠ©α΅›βˆ· A₁≑Aβ‚‚ $
         conv-βŠ©α΅›βˆ·
           (βŠ©α΅›β‰‘β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑²≑[]↑² A₁≑Aβ‚‚ $
            sucα΅› (varα΅› (there here) (wf-βŠ©α΅› (wf-βŠ©α΅›βˆ· ⊩u₁)) .projβ‚‚))
         ⊩uβ‚‚ of Ξ»
      ⊩uβ‚‚ β†’
    case wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ of Ξ»
      (βŠ©Οƒβ‚ , βŠ©Οƒβ‚‚) β†’

    case βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑] A₁≑Aβ‚‚ σ₁≑σ₂ of Ξ»
      A₁[σ₁⇑]≑Aβ‚‚[σ₂⇑] β†’
    case PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (singleSubstLift A₁ _) $
         βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t₁≑tβ‚‚ .projβ‚‚ σ₁≑σ₂ of Ξ»
      t₁[σ₁]≑tβ‚‚[Οƒβ‚‚] β†’
    case PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (natrecSucCase _ A₁) $
         βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑]∷ u₁≑uβ‚‚ σ₁≑σ₂ of Ξ»
      u₁[σ₁⇑⇑]≑uβ‚‚[σ₂⇑⇑] β†’

    case βŠ©β‰‘βˆ·β„•β‡” .proj₁ $
         βŠ©α΅›β‰‘βˆ·β‡” .proj₁ v₁≑vβ‚‚ .projβ‚‚ σ₁≑σ₂ of Ξ»
      (βŠ©β„•-v₁ , βŠ©β„•-vβ‚‚ , βŠ©β„•-v₁≑vβ‚‚) β†’

    PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (PE.sym $ singleSubstLift A₁ _) $
    ⊩natrec≑natrecβ€²
      (escape $ wf-βŠ©β‰‘ A₁[σ₁⇑]≑Aβ‚‚[σ₂⇑] .proj₁)
      (escape $ βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[⇑] ⊩Aβ‚‚ βŠ©Οƒβ‚‚)
      (escape-βŠ©β‰‘ A₁[σ₁⇑]≑Aβ‚‚[σ₂⇑])
      (βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ (refl-βŠ©α΅›β‰‘ ⊩A₁) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒβ‚))
      (βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ (refl-βŠ©α΅›β‰‘ ⊩Aβ‚‚) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒβ‚‚))
      (βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ A₁≑Aβ‚‚ σ₁≑σ₂)
      (escape-⊩∷ $ wf-βŠ©β‰‘βˆ· t₁[σ₁]≑tβ‚‚[Οƒβ‚‚] .proj₁)
      (PE.subst (_⊒_∷_ _ _) (singleSubstLift Aβ‚‚ _) $
       escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩tβ‚‚ βŠ©Οƒβ‚‚)
      (level-βŠ©β‰‘βˆ·
         (wf-βŠ©β‰‘
            (βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ A₁≑Aβ‚‚ σ₁≑σ₂ $
             refl-βŠ©β‰‘βˆ· $ ⊩zero {l = l} $ escape-⊩˒∷ βŠ©Οƒβ‚ .proj₁)
            .proj₁)
         t₁[σ₁]≑tβ‚‚[Οƒβ‚‚])
      (escape-⊩∷ $ wf-βŠ©β‰‘βˆ· u₁[σ₁⇑⇑]≑uβ‚‚[σ₂⇑⇑] .proj₁)
      (PE.subst (_⊒_∷_ _ _) (natrecSucCase _ Aβ‚‚) $
       escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[⇑⇑]∷ ⊩uβ‚‚ βŠ©Οƒβ‚‚)
      (escape-βŠ©β‰‘βˆ· u₁[σ₁⇑⇑]≑uβ‚‚[σ₂⇑⇑])
      (Ξ» {v₁ = v₁} {vβ‚‚ = _} {w₁ = w₁} v₁≑vβ‚‚ w₁≑wβ‚‚ β†’
         level-βŠ©β‰‘βˆ·
           (wf-βŠ©β‰‘
              (βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ A₁≑Aβ‚‚ σ₁≑σ₂ $
               ⊩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₁ ]β‚€                         ∎) $
         βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]β‚β‚€βˆ· u₁≑uβ‚‚ σ₁≑σ₂ v₁≑vβ‚‚ w₁≑wβ‚‚)
      βŠ©β„•-v₁ βŠ©β„•-vβ‚‚ βŠ©β„•-v₁≑vβ‚‚
    where
    open Tools.Reasoning.PropositionalEquality

opaque

  -- Validity of equality preservation for natrec.

  natrec-congα΅› :
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ l ⟩ A₁ ≑ Aβ‚‚ β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t₁ ≑ tβ‚‚ ∷ A₁ [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ 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β‚‚ t₁≑tβ‚‚ u₁≑uβ‚‚ v₁≑vβ‚‚ =
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚€ (wf-βŠ©α΅›β‰‘ A₁≑Aβ‚‚ .proj₁) (wf-βŠ©α΅›β‰‘βˆ· v₁≑vβ‚‚ .proj₁)
      , ⊩natrec≑natrec A₁≑Aβ‚‚ t₁≑tβ‚‚ u₁≑uβ‚‚ v₁≑vβ‚‚
      )

opaque

  -- Validity of natrec.

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

opaque

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

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

opaque

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

  natrec-sucα΅› :
    Ξ“ βˆ™ β„• βŠ©α΅›βŸ¨ lβ€² ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€³ ⟩ t ∷ A [ zero ]β‚€ β†’
    Ξ“ βˆ™ β„• βˆ™ 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 ⊩v =
    βŠ©α΅›βˆ·-⇐
      (Ξ» βŠ©Οƒ β†’
         PE.substβ‚‚ (_⊒_β‡’_∷_ _ _) (PE.sym $ [,]-[]-commute u)
           (PE.sym $ singleSubstLift A _) $
         natrec-suc
           (escape $ βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[⇑] ⊩A βŠ©Οƒ)
           (PE.subst (_⊒_∷_ _ _) (singleSubstLift A _) $
            escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩t βŠ©Οƒ)
           (PE.subst (_⊒_∷_ _ _) (natrecSucCase _ A) $
            escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[⇑⇑]∷ ⊩u βŠ©Οƒ)
           (escape-⊩∷ $ βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩v βŠ©Οƒ))
      (PE.subst (_βŠ©α΅›βŸ¨_⟩_∷_ _ _ _) (PE.sym $ substComp↑² A _) $
       βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚β‚€βˆ· ⊩u ⊩v (natrecα΅› ⊩A ⊩t ⊩u ⊩v))