module Definition.Untyped.Inversion {a} (M : Set a) where
open import Definition.Untyped M
open import Tools.Fin
open import Tools.Nat
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Sum
private variable
l : Term _
x : Fin _
α : Nat
ρ : Wk _ _
A B t t′ u v w : Term _
p q r : M
s : Strength
b : BinderMode
σ : Subst _ _
wk-var :
wk ρ t ≡ var x →
∃ λ x′ → t ≡ var x′ × wkVar ρ x′ ≡ x
wk-var {t = var _} refl = _ , refl , refl
wk-var {t = defn _} ()
wk-var {t = Level} ()
wk-var {t = zeroᵘ} ()
wk-var {t = sucᵘ _} ()
wk-var {t = _ supᵘ _} ()
wk-var {t = U _} ()
wk-var {t = Lift _ _} ()
wk-var {t = lift _} ()
wk-var {t = lower _} ()
wk-var {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-var {t = lam _ _} ()
wk-var {t = _ ∘⟨ _ ⟩ _} ()
wk-var {t = prod _ _ _ _} ()
wk-var {t = fst _ _} ()
wk-var {t = snd _ _} ()
wk-var {t = prodrec _ _ _ _ _ _} ()
wk-var {t = Empty} ()
wk-var {t = emptyrec _ _ _} ()
wk-var {t = Unit _} ()
wk-var {t = star _} ()
wk-var {t = unitrec _ _ _ _ _} ()
wk-var {t = ℕ} ()
wk-var {t = zero} ()
wk-var {t = suc _} ()
wk-var {t = natrec _ _ _ _ _ _ _} ()
wk-var {t = Id _ _ _} ()
wk-var {t = rfl} ()
wk-var {t = J _ _ _ _ _ _ _ _} ()
wk-var {t = K _ _ _ _ _ _} ()
wk-var {t = []-cong _ _ _ _ _ _} ()
subst-var :
t [ σ ] ≡ var x →
∃ λ x′ → t ≡ var x′ × σ x′ ≡ var x
subst-var {t = var _} eq = _ , refl , eq
subst-var {t = defn _} ()
subst-var {t = Level} ()
subst-var {t = zeroᵘ} ()
subst-var {t = sucᵘ _} ()
subst-var {t = _ supᵘ _} ()
subst-var {t = U _} ()
subst-var {t = Lift _ _} ()
subst-var {t = lift _} ()
subst-var {t = lower _} ()
subst-var {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-var {t = lam _ _} ()
subst-var {t = _ ∘⟨ _ ⟩ _} ()
subst-var {t = prod _ _ _ _} ()
subst-var {t = fst _ _} ()
subst-var {t = snd _ _} ()
subst-var {t = prodrec _ _ _ _ _ _} ()
subst-var {t = Empty} ()
subst-var {t = emptyrec _ _ _} ()
subst-var {t = Unit _} ()
subst-var {t = star _} ()
subst-var {t = unitrec _ _ _ _ _} ()
subst-var {t = ℕ} ()
subst-var {t = zero} ()
subst-var {t = suc _} ()
subst-var {t = natrec _ _ _ _ _ _ _} ()
subst-var {t = Id _ _ _} ()
subst-var {t = rfl} ()
subst-var {t = J _ _ _ _ _ _ _ _} ()
subst-var {t = K _ _ _ _ _ _} ()
subst-var {t = []-cong _ _ _ _ _ _} ()
wk-Level : wk ρ t ≡ Level → t ≡ Level
wk-Level {t = Level} refl = refl
wk-Level {t = var _} ()
wk-Level {t = defn _} ()
wk-Level {t = zeroᵘ} ()
wk-Level {t = sucᵘ _} ()
wk-Level {t = _ supᵘ _} ()
wk-Level {t = U _} ()
wk-Level {t = Lift _ _} ()
wk-Level {t = lift _} ()
wk-Level {t = lower _} ()
wk-Level {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-Level {t = lam _ _} ()
wk-Level {t = _ ∘⟨ _ ⟩ _} ()
wk-Level {t = prod _ _ _ _} ()
wk-Level {t = fst _ _} ()
wk-Level {t = snd _ _} ()
wk-Level {t = prodrec _ _ _ _ _ _} ()
wk-Level {t = Empty} ()
wk-Level {t = emptyrec _ _ _} ()
wk-Level {t = Unit _} ()
wk-Level {t = star _} ()
wk-Level {t = unitrec _ _ _ _ _} ()
wk-Level {t = ℕ} ()
wk-Level {t = zero} ()
wk-Level {t = suc _} ()
wk-Level {t = natrec _ _ _ _ _ _ _} ()
wk-Level {t = Id _ _ _} ()
wk-Level {t = rfl} ()
wk-Level {t = J _ _ _ _ _ _ _ _} ()
wk-Level {t = K _ _ _ _ _ _} ()
wk-Level {t = []-cong _ _ _ _ _ _} ()
subst-Level : t [ σ ] ≡ Level → (∃ λ x → t ≡ var x) ⊎ t ≡ Level
subst-Level {t = var _} _ = inj₁ (_ , refl)
subst-Level {t = Level} refl = inj₂ refl
subst-Level {t = defn _} ()
subst-Level {t = zeroᵘ} ()
subst-Level {t = sucᵘ _} ()
subst-Level {t = _ supᵘ _} ()
subst-Level {t = U _} ()
subst-Level {t = Lift _ _} ()
subst-Level {t = lift _} ()
subst-Level {t = lower _} ()
subst-Level {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-Level {t = lam _ _} ()
subst-Level {t = _ ∘⟨ _ ⟩ _} ()
subst-Level {t = prod _ _ _ _} ()
subst-Level {t = fst _ _} ()
subst-Level {t = snd _ _} ()
subst-Level {t = prodrec _ _ _ _ _ _} ()
subst-Level {t = Empty} ()
subst-Level {t = emptyrec _ _ _} ()
subst-Level {t = Unit _} ()
subst-Level {t = star _} ()
subst-Level {t = unitrec _ _ _ _ _} ()
subst-Level {t = ℕ} ()
subst-Level {t = zero} ()
subst-Level {t = suc _} ()
subst-Level {t = natrec _ _ _ _ _ _ _} ()
subst-Level {t = Id _ _ _} ()
subst-Level {t = rfl} ()
subst-Level {t = J _ _ _ _ _ _ _ _} ()
subst-Level {t = K _ _ _ _ _ _} ()
subst-Level {t = []-cong _ _ _ _ _ _} ()
wk-zeroᵘ : wk ρ t ≡ zeroᵘ → t ≡ zeroᵘ
wk-zeroᵘ {t = zeroᵘ} refl = refl
wk-zeroᵘ {t = var _} ()
wk-zeroᵘ {t = defn _} ()
wk-zeroᵘ {t = Level} ()
wk-zeroᵘ {t = sucᵘ _} ()
wk-zeroᵘ {t = _ supᵘ _} ()
wk-zeroᵘ {t = U _} ()
wk-zeroᵘ {t = Lift _ _} ()
wk-zeroᵘ {t = lift _} ()
wk-zeroᵘ {t = lower _} ()
wk-zeroᵘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-zeroᵘ {t = lam _ _} ()
wk-zeroᵘ {t = _ ∘⟨ _ ⟩ _} ()
wk-zeroᵘ {t = prod _ _ _ _} ()
wk-zeroᵘ {t = fst _ _} ()
wk-zeroᵘ {t = snd _ _} ()
wk-zeroᵘ {t = prodrec _ _ _ _ _ _} ()
wk-zeroᵘ {t = Empty} ()
wk-zeroᵘ {t = emptyrec _ _ _} ()
wk-zeroᵘ {t = Unit _} ()
wk-zeroᵘ {t = star _} ()
wk-zeroᵘ {t = unitrec _ _ _ _ _} ()
wk-zeroᵘ {t = ℕ} ()
wk-zeroᵘ {t = zero} ()
wk-zeroᵘ {t = suc _} ()
wk-zeroᵘ {t = natrec _ _ _ _ _ _ _} ()
wk-zeroᵘ {t = Id _ _ _} ()
wk-zeroᵘ {t = rfl} ()
wk-zeroᵘ {t = J _ _ _ _ _ _ _ _} ()
wk-zeroᵘ {t = K _ _ _ _ _ _} ()
wk-zeroᵘ {t = []-cong _ _ _ _ _ _} ()
subst-zeroᵘ : t [ σ ] ≡ zeroᵘ → (∃ λ x → t ≡ var x) ⊎ t ≡ zeroᵘ
subst-zeroᵘ {t = var _} _ = inj₁ (_ , refl)
subst-zeroᵘ {t = zeroᵘ} refl = inj₂ refl
subst-zeroᵘ {t = defn _} ()
subst-zeroᵘ {t = Level} ()
subst-zeroᵘ {t = sucᵘ _} ()
subst-zeroᵘ {t = _ supᵘ _} ()
subst-zeroᵘ {t = U _} ()
subst-zeroᵘ {t = Lift _ _} ()
subst-zeroᵘ {t = lift _} ()
subst-zeroᵘ {t = lower _} ()
subst-zeroᵘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-zeroᵘ {t = lam _ _} ()
subst-zeroᵘ {t = _ ∘⟨ _ ⟩ _} ()
subst-zeroᵘ {t = prod _ _ _ _} ()
subst-zeroᵘ {t = fst _ _} ()
subst-zeroᵘ {t = snd _ _} ()
subst-zeroᵘ {t = prodrec _ _ _ _ _ _} ()
subst-zeroᵘ {t = Empty} ()
subst-zeroᵘ {t = emptyrec _ _ _} ()
subst-zeroᵘ {t = Unit _} ()
subst-zeroᵘ {t = star _} ()
subst-zeroᵘ {t = unitrec _ _ _ _ _} ()
subst-zeroᵘ {t = ℕ} ()
subst-zeroᵘ {t = zero} ()
subst-zeroᵘ {t = suc _} ()
subst-zeroᵘ {t = natrec _ _ _ _ _ _ _} ()
subst-zeroᵘ {t = Id _ _ _} ()
subst-zeroᵘ {t = rfl} ()
subst-zeroᵘ {t = J _ _ _ _ _ _ _ _} ()
subst-zeroᵘ {t = K _ _ _ _ _ _} ()
subst-zeroᵘ {t = []-cong _ _ _ _ _ _} ()
wk-sucᵘ :
wk ρ t ≡ sucᵘ u →
∃ λ u′ → t ≡ sucᵘ u′ × wk ρ u′ ≡ u
wk-sucᵘ {t = sucᵘ _} refl = _ , refl , refl
wk-sucᵘ {t = var _} ()
wk-sucᵘ {t = defn _} ()
wk-sucᵘ {t = Level} ()
wk-sucᵘ {t = zeroᵘ} ()
wk-sucᵘ {t = _ supᵘ _} ()
wk-sucᵘ {t = U _} ()
wk-sucᵘ {t = Lift _ _} ()
wk-sucᵘ {t = lift _} ()
wk-sucᵘ {t = lower _} ()
wk-sucᵘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-sucᵘ {t = lam _ _} ()
wk-sucᵘ {t = _ ∘⟨ _ ⟩ _} ()
wk-sucᵘ {t = prod _ _ _ _} ()
wk-sucᵘ {t = fst _ _} ()
wk-sucᵘ {t = snd _ _} ()
wk-sucᵘ {t = prodrec _ _ _ _ _ _} ()
wk-sucᵘ {t = Empty} ()
wk-sucᵘ {t = emptyrec _ _ _} ()
wk-sucᵘ {t = Unit _} ()
wk-sucᵘ {t = star _} ()
wk-sucᵘ {t = unitrec _ _ _ _ _} ()
wk-sucᵘ {t = ℕ} ()
wk-sucᵘ {t = zero} ()
wk-sucᵘ {t = suc _} ()
wk-sucᵘ {t = natrec _ _ _ _ _ _ _} ()
wk-sucᵘ {t = Id _ _ _} ()
wk-sucᵘ {t = rfl} ()
wk-sucᵘ {t = J _ _ _ _ _ _ _ _} ()
wk-sucᵘ {t = K _ _ _ _ _ _} ()
wk-sucᵘ {t = []-cong _ _ _ _ _ _} ()
subst-sucᵘ :
t [ σ ] ≡ sucᵘ u →
(∃ λ x → t ≡ var x) ⊎ ∃ λ u′ → t ≡ sucᵘ u′ × u′ [ σ ] ≡ u
subst-sucᵘ {t = var _} _ = inj₁ (_ , refl)
subst-sucᵘ {t = sucᵘ _} refl = inj₂ (_ , refl , refl)
subst-sucᵘ {t = defn _} ()
subst-sucᵘ {t = Level} ()
subst-sucᵘ {t = zeroᵘ} ()
subst-sucᵘ {t = _ supᵘ _} ()
subst-sucᵘ {t = U _} ()
subst-sucᵘ {t = Lift _ _} ()
subst-sucᵘ {t = lift _} ()
subst-sucᵘ {t = lower _} ()
subst-sucᵘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-sucᵘ {t = lam _ _} ()
subst-sucᵘ {t = _ ∘⟨ _ ⟩ _} ()
subst-sucᵘ {t = prod _ _ _ _} ()
subst-sucᵘ {t = fst _ _} ()
subst-sucᵘ {t = snd _ _} ()
subst-sucᵘ {t = prodrec _ _ _ _ _ _} ()
subst-sucᵘ {t = Empty} ()
subst-sucᵘ {t = emptyrec _ _ _} ()
subst-sucᵘ {t = Unit _} ()
subst-sucᵘ {t = star _} ()
subst-sucᵘ {t = unitrec _ _ _ _ _} ()
subst-sucᵘ {t = ℕ} ()
subst-sucᵘ {t = zero} ()
subst-sucᵘ {t = suc _} ()
subst-sucᵘ {t = natrec _ _ _ _ _ _ _} ()
subst-sucᵘ {t = Id _ _ _} ()
subst-sucᵘ {t = rfl} ()
subst-sucᵘ {t = J _ _ _ _ _ _ _ _} ()
subst-sucᵘ {t = K _ _ _ _ _ _} ()
subst-sucᵘ {t = []-cong _ _ _ _ _ _} ()
wk-supᵘ :
wk ρ t ≡ u supᵘ v →
∃₂ λ u′ v′ → t ≡ u′ supᵘ v′ × wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-supᵘ {t = _ supᵘ _} refl = _ , _ , refl , refl , refl
wk-supᵘ {t = defn _} ()
wk-supᵘ {t = Level} ()
wk-supᵘ {t = zeroᵘ} ()
wk-supᵘ {t = sucᵘ _} ()
wk-supᵘ {t = U _} ()
wk-supᵘ {t = Lift _ _} ()
wk-supᵘ {t = lift _} ()
wk-supᵘ {t = lower _} ()
wk-supᵘ {t = var _} ()
wk-supᵘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-supᵘ {t = lam _ _} ()
wk-supᵘ {t = _ ∘⟨ _ ⟩ _} ()
wk-supᵘ {t = prod _ _ _ _} ()
wk-supᵘ {t = fst _ _} ()
wk-supᵘ {t = snd _ _} ()
wk-supᵘ {t = prodrec _ _ _ _ _ _} ()
wk-supᵘ {t = Empty} ()
wk-supᵘ {t = emptyrec _ _ _} ()
wk-supᵘ {t = Unit _} ()
wk-supᵘ {t = star _} ()
wk-supᵘ {t = unitrec _ _ _ _ _} ()
wk-supᵘ {t = ℕ} ()
wk-supᵘ {t = zero} ()
wk-supᵘ {t = suc _} ()
wk-supᵘ {t = natrec _ _ _ _ _ _ _} ()
wk-supᵘ {t = Id _ _ _} ()
wk-supᵘ {t = rfl} ()
wk-supᵘ {t = J _ _ _ _ _ _ _ _} ()
wk-supᵘ {t = K _ _ _ _ _ _} ()
wk-supᵘ {t = []-cong _ _ _ _ _ _} ()
subst-supᵘ :
t [ σ ] ≡ u supᵘ v →
(∃ λ x → t ≡ var x) ⊎
∃₂ λ u′ v′ → t ≡ u′ supᵘ v′ × u′ [ σ ] ≡ u × v′ [ σ ] ≡ v
subst-supᵘ {t = var _} _ = inj₁ (_ , refl)
subst-supᵘ {t = _ supᵘ _} refl = inj₂ (_ , _ , refl , refl , refl)
subst-supᵘ {t = defn _} ()
subst-supᵘ {t = Level} ()
subst-supᵘ {t = zeroᵘ} ()
subst-supᵘ {t = sucᵘ _} ()
subst-supᵘ {t = U _} ()
subst-supᵘ {t = Lift _ _} ()
subst-supᵘ {t = lift _} ()
subst-supᵘ {t = lower _} ()
subst-supᵘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-supᵘ {t = lam _ _} ()
subst-supᵘ {t = _ ∘⟨ _ ⟩ _} ()
subst-supᵘ {t = prod _ _ _ _} ()
subst-supᵘ {t = fst _ _} ()
subst-supᵘ {t = snd _ _} ()
subst-supᵘ {t = prodrec _ _ _ _ _ _} ()
subst-supᵘ {t = Empty} ()
subst-supᵘ {t = emptyrec _ _ _} ()
subst-supᵘ {t = Unit _} ()
subst-supᵘ {t = star _} ()
subst-supᵘ {t = unitrec _ _ _ _ _} ()
subst-supᵘ {t = ℕ} ()
subst-supᵘ {t = zero} ()
subst-supᵘ {t = suc _} ()
subst-supᵘ {t = natrec _ _ _ _ _ _ _} ()
subst-supᵘ {t = Id _ _ _} ()
subst-supᵘ {t = rfl} ()
subst-supᵘ {t = J _ _ _ _ _ _ _ _} ()
subst-supᵘ {t = K _ _ _ _ _ _} ()
subst-supᵘ {t = []-cong _ _ _ _ _ _} ()
wk-defn : wk ρ t ≡ defn α → t ≡ defn α
wk-defn {t = defn α} refl = refl
wk-defn {t = var _} ()
wk-defn {t = Level} ()
wk-defn {t = zeroᵘ} ()
wk-defn {t = sucᵘ _} ()
wk-defn {t = _ supᵘ _} ()
wk-defn {t = U _} ()
wk-defn {t = Lift _ _} ()
wk-defn {t = lift _} ()
wk-defn {t = lower _} ()
wk-defn {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-defn {t = lam _ _} ()
wk-defn {t = _ ∘⟨ _ ⟩ _} ()
wk-defn {t = prod _ _ _ _} ()
wk-defn {t = fst _ _} ()
wk-defn {t = snd _ _} ()
wk-defn {t = prodrec _ _ _ _ _ _} ()
wk-defn {t = Empty} ()
wk-defn {t = emptyrec _ _ _} ()
wk-defn {t = Unit _} ()
wk-defn {t = star _} ()
wk-defn {t = unitrec _ _ _ _ _} ()
wk-defn {t = ℕ} ()
wk-defn {t = zero} ()
wk-defn {t = suc _} ()
wk-defn {t = natrec _ _ _ _ _ _ _} ()
wk-defn {t = Id _ _ _} ()
wk-defn {t = rfl} ()
wk-defn {t = J _ _ _ _ _ _ _ _} ()
wk-defn {t = K _ _ _ _ _ _} ()
wk-defn {t = []-cong _ _ _ _ _ _} ()
subst-defn : t [ σ ] ≡ defn α → (∃ λ x → t ≡ var x) ⊎ t ≡ defn α
subst-defn {t = var _} _ = inj₁ (_ , refl)
subst-defn {t = defn α} refl = inj₂ refl
subst-defn {t = Level} ()
subst-defn {t = zeroᵘ} ()
subst-defn {t = sucᵘ _} ()
subst-defn {t = _ supᵘ _} ()
subst-defn {t = U _} ()
subst-defn {t = Lift _ _} ()
subst-defn {t = lift _} ()
subst-defn {t = lower _} ()
subst-defn {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-defn {t = lam _ _} ()
subst-defn {t = _ ∘⟨ _ ⟩ _} ()
subst-defn {t = prod _ _ _ _} ()
subst-defn {t = fst _ _} ()
subst-defn {t = snd _ _} ()
subst-defn {t = prodrec _ _ _ _ _ _} ()
subst-defn {t = Empty} ()
subst-defn {t = emptyrec _ _ _} ()
subst-defn {t = Unit _} ()
subst-defn {t = star _} ()
subst-defn {t = unitrec _ _ _ _ _} ()
subst-defn {t = ℕ} ()
subst-defn {t = zero} ()
subst-defn {t = suc _} ()
subst-defn {t = natrec _ _ _ _ _ _ _} ()
subst-defn {t = Id _ _ _} ()
subst-defn {t = rfl} ()
subst-defn {t = J _ _ _ _ _ _ _ _} ()
subst-defn {t = K _ _ _ _ _ _} ()
subst-defn {t = []-cong _ _ _ _ _ _} ()
wk-U : wk ρ t ≡ U l → ∃ λ l′ → t ≡ U l′ × wk ρ l′ ≡ l
wk-U {t = U l} refl = _ , refl , refl
wk-U {t = Level} ()
wk-U {t = zeroᵘ} ()
wk-U {t = sucᵘ _} ()
wk-U {t = _ supᵘ _} ()
wk-U {t = var _} ()
wk-U {t = defn _} ()
wk-U {t = Lift _ _} ()
wk-U {t = lift _} ()
wk-U {t = lower _} ()
wk-U {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-U {t = lam _ _} ()
wk-U {t = _ ∘⟨ _ ⟩ _} ()
wk-U {t = prod _ _ _ _} ()
wk-U {t = fst _ _} ()
wk-U {t = snd _ _} ()
wk-U {t = prodrec _ _ _ _ _ _} ()
wk-U {t = Empty} ()
wk-U {t = emptyrec _ _ _} ()
wk-U {t = Unit _} ()
wk-U {t = star _} ()
wk-U {t = unitrec _ _ _ _ _} ()
wk-U {t = ℕ} ()
wk-U {t = zero} ()
wk-U {t = suc _} ()
wk-U {t = natrec _ _ _ _ _ _ _} ()
wk-U {t = Id _ _ _} ()
wk-U {t = rfl} ()
wk-U {t = J _ _ _ _ _ _ _ _} ()
wk-U {t = K _ _ _ _ _ _} ()
wk-U {t = []-cong _ _ _ _ _ _} ()
subst-U : t [ σ ] ≡ U l → (∃ λ x → t ≡ var x) ⊎ ∃ λ l′ → t ≡ U l′ × l′ [ σ ] ≡ l
subst-U {t = var _} _ = inj₁ (_ , refl)
subst-U {t = defn _} ()
subst-U {t = U _} refl = inj₂ (_ , refl , refl)
subst-U {t = Level} ()
subst-U {t = zeroᵘ} ()
subst-U {t = sucᵘ _} ()
subst-U {t = _ supᵘ _} ()
subst-U {t = Lift _ _} ()
subst-U {t = lift _} ()
subst-U {t = lower _} ()
subst-U {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-U {t = lam _ _} ()
subst-U {t = _ ∘⟨ _ ⟩ _} ()
subst-U {t = prod _ _ _ _} ()
subst-U {t = fst _ _} ()
subst-U {t = snd _ _} ()
subst-U {t = prodrec _ _ _ _ _ _} ()
subst-U {t = Empty} ()
subst-U {t = emptyrec _ _ _} ()
subst-U {t = Unit _} ()
subst-U {t = star _} ()
subst-U {t = unitrec _ _ _ _ _} ()
subst-U {t = ℕ} ()
subst-U {t = zero} ()
subst-U {t = suc _} ()
subst-U {t = natrec _ _ _ _ _ _ _} ()
subst-U {t = Id _ _ _} ()
subst-U {t = rfl} ()
subst-U {t = J _ _ _ _ _ _ _ _} ()
subst-U {t = K _ _ _ _ _ _} ()
subst-U {t = []-cong _ _ _ _ _ _} ()
wk-Lift : wk ρ t ≡ Lift l A → ∃₂ λ l′ A′ → t ≡ Lift l′ A′ × wk ρ l′ ≡ l × wk ρ A′ ≡ A
wk-Lift {t = defn _} ()
wk-Lift {t = U l} ()
wk-Lift {t = Level} ()
wk-Lift {t = zeroᵘ} ()
wk-Lift {t = sucᵘ _} ()
wk-Lift {t = _ supᵘ _} ()
wk-Lift {t = var _} ()
wk-Lift {t = Lift _ _} refl = _ , _ , refl , refl , refl
wk-Lift {t = lift _} ()
wk-Lift {t = lower _} ()
wk-Lift {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-Lift {t = lam _ _} ()
wk-Lift {t = _ ∘⟨ _ ⟩ _} ()
wk-Lift {t = prod _ _ _ _} ()
wk-Lift {t = fst _ _} ()
wk-Lift {t = snd _ _} ()
wk-Lift {t = prodrec _ _ _ _ _ _} ()
wk-Lift {t = Empty} ()
wk-Lift {t = emptyrec _ _ _} ()
wk-Lift {t = Unit _} ()
wk-Lift {t = star _} ()
wk-Lift {t = unitrec _ _ _ _ _} ()
wk-Lift {t = ℕ} ()
wk-Lift {t = zero} ()
wk-Lift {t = suc _} ()
wk-Lift {t = natrec _ _ _ _ _ _ _} ()
wk-Lift {t = Id _ _ _} ()
wk-Lift {t = rfl} ()
wk-Lift {t = J _ _ _ _ _ _ _ _} ()
wk-Lift {t = K _ _ _ _ _ _} ()
wk-Lift {t = []-cong _ _ _ _ _ _} ()
subst-Lift : t [ σ ] ≡ Lift l A → (∃ λ x → t ≡ var x) ⊎ ∃₂ λ l′ A′ → t ≡ Lift l′ A′ × l′ [ σ ] ≡ l × A′ [ σ ] ≡ A
subst-Lift {t = var _} _ = inj₁ (_ , refl)
subst-Lift {t = defn _} ()
subst-Lift {t = U _} ()
subst-Lift {t = Level} ()
subst-Lift {t = zeroᵘ} ()
subst-Lift {t = sucᵘ _} ()
subst-Lift {t = _ supᵘ _} ()
subst-Lift {t = Lift _ _} refl = inj₂ (_ , _ , refl , refl , refl)
subst-Lift {t = lift _} ()
subst-Lift {t = lower _} ()
subst-Lift {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-Lift {t = lam _ _} ()
subst-Lift {t = _ ∘⟨ _ ⟩ _} ()
subst-Lift {t = prod _ _ _ _} ()
subst-Lift {t = fst _ _} ()
subst-Lift {t = snd _ _} ()
subst-Lift {t = prodrec _ _ _ _ _ _} ()
subst-Lift {t = Empty} ()
subst-Lift {t = emptyrec _ _ _} ()
subst-Lift {t = Unit _} ()
subst-Lift {t = star _} ()
subst-Lift {t = unitrec _ _ _ _ _} ()
subst-Lift {t = ℕ} ()
subst-Lift {t = zero} ()
subst-Lift {t = suc _} ()
subst-Lift {t = natrec _ _ _ _ _ _ _} ()
subst-Lift {t = Id _ _ _} ()
subst-Lift {t = rfl} ()
subst-Lift {t = J _ _ _ _ _ _ _ _} ()
subst-Lift {t = K _ _ _ _ _ _} ()
subst-Lift {t = []-cong _ _ _ _ _ _} ()
wk-lift : wk ρ t ≡ lift A → ∃ λ A′ → t ≡ lift A′ × wk ρ A′ ≡ A
wk-lift {t = defn _} ()
wk-lift {t = U l} ()
wk-lift {t = Level} ()
wk-lift {t = zeroᵘ} ()
wk-lift {t = sucᵘ _} ()
wk-lift {t = _ supᵘ _} ()
wk-lift {t = var _} ()
wk-lift {t = Lift _ _} ()
wk-lift {t = lift _} refl = _ , refl , refl
wk-lift {t = lower _} ()
wk-lift {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-lift {t = lam _ _} ()
wk-lift {t = _ ∘⟨ _ ⟩ _} ()
wk-lift {t = prod _ _ _ _} ()
wk-lift {t = fst _ _} ()
wk-lift {t = snd _ _} ()
wk-lift {t = prodrec _ _ _ _ _ _} ()
wk-lift {t = Empty} ()
wk-lift {t = emptyrec _ _ _} ()
wk-lift {t = Unit _} ()
wk-lift {t = star _} ()
wk-lift {t = unitrec _ _ _ _ _} ()
wk-lift {t = ℕ} ()
wk-lift {t = zero} ()
wk-lift {t = suc _} ()
wk-lift {t = natrec _ _ _ _ _ _ _} ()
wk-lift {t = Id _ _ _} ()
wk-lift {t = rfl} ()
wk-lift {t = J _ _ _ _ _ _ _ _} ()
wk-lift {t = K _ _ _ _ _ _} ()
wk-lift {t = []-cong _ _ _ _ _ _} ()
subst-lift : t [ σ ] ≡ lift A → (∃ λ x → t ≡ var x) ⊎ ∃ λ A′ → t ≡ lift A′ × A′ [ σ ] ≡ A
subst-lift {t = var _} _ = inj₁ (_ , refl)
subst-lift {t = defn _} ()
subst-lift {t = U _} ()
subst-lift {t = Level} ()
subst-lift {t = zeroᵘ} ()
subst-lift {t = sucᵘ _} ()
subst-lift {t = _ supᵘ _} ()
subst-lift {t = Lift _ _} ()
subst-lift {t = lift _} refl = inj₂ (_ , refl , refl)
subst-lift {t = lower _} ()
subst-lift {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-lift {t = lam _ _} ()
subst-lift {t = _ ∘⟨ _ ⟩ _} ()
subst-lift {t = prod _ _ _ _} ()
subst-lift {t = fst _ _} ()
subst-lift {t = snd _ _} ()
subst-lift {t = prodrec _ _ _ _ _ _} ()
subst-lift {t = Empty} ()
subst-lift {t = emptyrec _ _ _} ()
subst-lift {t = Unit _} ()
subst-lift {t = star _} ()
subst-lift {t = unitrec _ _ _ _ _} ()
subst-lift {t = ℕ} ()
subst-lift {t = zero} ()
subst-lift {t = suc _} ()
subst-lift {t = natrec _ _ _ _ _ _ _} ()
subst-lift {t = Id _ _ _} ()
subst-lift {t = rfl} ()
subst-lift {t = J _ _ _ _ _ _ _ _} ()
subst-lift {t = K _ _ _ _ _ _} ()
subst-lift {t = []-cong _ _ _ _ _ _} ()
wk-lower : wk ρ t ≡ lower u → ∃ λ u′ → t ≡ lower u′ × wk ρ u′ ≡ u
wk-lower {t = defn _} ()
wk-lower {t = U l} ()
wk-lower {t = Level} ()
wk-lower {t = zeroᵘ} ()
wk-lower {t = sucᵘ _} ()
wk-lower {t = _ supᵘ _} ()
wk-lower {t = var _} ()
wk-lower {t = Lift _ _} ()
wk-lower {t = lift _} ()
wk-lower {t = lower _} refl = _ , refl , refl
wk-lower {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-lower {t = lam _ _} ()
wk-lower {t = _ ∘⟨ _ ⟩ _} ()
wk-lower {t = prod _ _ _ _} ()
wk-lower {t = fst _ _} ()
wk-lower {t = snd _ _} ()
wk-lower {t = prodrec _ _ _ _ _ _} ()
wk-lower {t = Empty} ()
wk-lower {t = emptyrec _ _ _} ()
wk-lower {t = Unit _} ()
wk-lower {t = star _} ()
wk-lower {t = unitrec _ _ _ _ _} ()
wk-lower {t = ℕ} ()
wk-lower {t = zero} ()
wk-lower {t = suc _} ()
wk-lower {t = natrec _ _ _ _ _ _ _} ()
wk-lower {t = Id _ _ _} ()
wk-lower {t = rfl} ()
wk-lower {t = J _ _ _ _ _ _ _ _} ()
wk-lower {t = K _ _ _ _ _ _} ()
wk-lower {t = []-cong _ _ _ _ _ _} ()
subst-lower : t [ σ ] ≡ lower u → (∃ λ x → t ≡ var x) ⊎ ∃ λ u′ → t ≡ lower u′ × u′ [ σ ] ≡ u
subst-lower {t = var _} _ = inj₁ (_ , refl)
subst-lower {t = defn _} ()
subst-lower {t = U _} ()
subst-lower {t = Level} ()
subst-lower {t = zeroᵘ} ()
subst-lower {t = sucᵘ _} ()
subst-lower {t = _ supᵘ _} ()
subst-lower {t = Lift _ _} ()
subst-lower {t = lift _} ()
subst-lower {t = lower _} refl = inj₂ (_ , refl , refl)
subst-lower {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-lower {t = lam _ _} ()
subst-lower {t = _ ∘⟨ _ ⟩ _} ()
subst-lower {t = prod _ _ _ _} ()
subst-lower {t = fst _ _} ()
subst-lower {t = snd _ _} ()
subst-lower {t = prodrec _ _ _ _ _ _} ()
subst-lower {t = Empty} ()
subst-lower {t = emptyrec _ _ _} ()
subst-lower {t = Unit _} ()
subst-lower {t = star _} ()
subst-lower {t = unitrec _ _ _ _ _} ()
subst-lower {t = ℕ} ()
subst-lower {t = zero} ()
subst-lower {t = suc _} ()
subst-lower {t = natrec _ _ _ _ _ _ _} ()
subst-lower {t = Id _ _ _} ()
subst-lower {t = rfl} ()
subst-lower {t = J _ _ _ _ _ _ _ _} ()
subst-lower {t = K _ _ _ _ _ _} ()
subst-lower {t = []-cong _ _ _ _ _ _} ()
wk-ΠΣ :
wk ρ t ≡ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B →
∃₂ λ A′ B′ →
t ≡ ΠΣ⟨ b ⟩ p , q ▷ A′ ▹ B′ ×
wk ρ A′ ≡ A × wk (lift ρ) B′ ≡ B
wk-ΠΣ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} refl =
_ , _ , refl , refl , refl
wk-ΠΣ {t = Level} ()
wk-ΠΣ {t = zeroᵘ} ()
wk-ΠΣ {t = sucᵘ _} ()
wk-ΠΣ {t = _ supᵘ _} ()
wk-ΠΣ {t = var _} ()
wk-ΠΣ {t = defn _} ()
wk-ΠΣ {t = U _} ()
wk-ΠΣ {t = Lift _ _} ()
wk-ΠΣ {t = lift _} ()
wk-ΠΣ {t = lower _} ()
wk-ΠΣ {t = lam _ _} ()
wk-ΠΣ {t = _ ∘⟨ _ ⟩ _} ()
wk-ΠΣ {t = prod _ _ _ _} ()
wk-ΠΣ {t = fst _ _} ()
wk-ΠΣ {t = snd _ _} ()
wk-ΠΣ {t = prodrec _ _ _ _ _ _} ()
wk-ΠΣ {t = Empty} ()
wk-ΠΣ {t = emptyrec _ _ _} ()
wk-ΠΣ {t = Unit _} ()
wk-ΠΣ {t = star _} ()
wk-ΠΣ {t = unitrec _ _ _ _ _} ()
wk-ΠΣ {t = ℕ} ()
wk-ΠΣ {t = zero} ()
wk-ΠΣ {t = suc _} ()
wk-ΠΣ {t = natrec _ _ _ _ _ _ _} ()
wk-ΠΣ {t = Id _ _ _} ()
wk-ΠΣ {t = rfl} ()
wk-ΠΣ {t = J _ _ _ _ _ _ _ _} ()
wk-ΠΣ {t = K _ _ _ _ _ _} ()
wk-ΠΣ {t = []-cong _ _ _ _ _ _} ()
subst-ΠΣ :
t [ σ ] ≡ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B →
(∃ λ x → t ≡ var x) ⊎
∃₂ λ A′ B′ →
t ≡ ΠΣ⟨ b ⟩ p , q ▷ A′ ▹ B′ ×
A′ [ σ ] ≡ A × B′ [ liftSubst σ ] ≡ B
subst-ΠΣ {t = var _} _ =
inj₁ (_ , refl)
subst-ΠΣ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} refl =
inj₂ (_ , _ , refl , refl , refl)
subst-ΠΣ {t = defn _} ()
subst-ΠΣ {t = Level} ()
subst-ΠΣ {t = zeroᵘ} ()
subst-ΠΣ {t = sucᵘ _} ()
subst-ΠΣ {t = _ supᵘ _} ()
subst-ΠΣ {t = U _} ()
subst-ΠΣ {t = Lift _ _} ()
subst-ΠΣ {t = lift _} ()
subst-ΠΣ {t = lower _} ()
subst-ΠΣ {t = lam _ _} ()
subst-ΠΣ {t = _ ∘⟨ _ ⟩ _} ()
subst-ΠΣ {t = prod _ _ _ _} ()
subst-ΠΣ {t = fst _ _} ()
subst-ΠΣ {t = snd _ _} ()
subst-ΠΣ {t = prodrec _ _ _ _ _ _} ()
subst-ΠΣ {t = Empty} ()
subst-ΠΣ {t = emptyrec _ _ _} ()
subst-ΠΣ {t = Unit _} ()
subst-ΠΣ {t = star _} ()
subst-ΠΣ {t = unitrec _ _ _ _ _} ()
subst-ΠΣ {t = ℕ} ()
subst-ΠΣ {t = zero} ()
subst-ΠΣ {t = suc _} ()
subst-ΠΣ {t = natrec _ _ _ _ _ _ _} ()
subst-ΠΣ {t = Id _ _ _} ()
subst-ΠΣ {t = rfl} ()
subst-ΠΣ {t = J _ _ _ _ _ _ _ _} ()
subst-ΠΣ {t = K _ _ _ _ _ _} ()
subst-ΠΣ {t = []-cong _ _ _ _ _ _} ()
wk-lam :
wk ρ t ≡ lam p u →
∃ λ u′ → t ≡ lam p u′ × wk (lift ρ) u′ ≡ u
wk-lam {t = lam _ _} refl = _ , refl , refl
wk-lam {t = var _} ()
wk-lam {t = defn _} ()
wk-lam {t = Level} ()
wk-lam {t = zeroᵘ} ()
wk-lam {t = sucᵘ _} ()
wk-lam {t = _ supᵘ _} ()
wk-lam {t = U _} ()
wk-lam {t = Lift _ _} ()
wk-lam {t = lift _} ()
wk-lam {t = lower _} ()
wk-lam {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-lam {t = _ ∘⟨ _ ⟩ _} ()
wk-lam {t = prod _ _ _ _} ()
wk-lam {t = fst _ _} ()
wk-lam {t = snd _ _} ()
wk-lam {t = prodrec _ _ _ _ _ _} ()
wk-lam {t = Empty} ()
wk-lam {t = emptyrec _ _ _} ()
wk-lam {t = Unit _} ()
wk-lam {t = star _} ()
wk-lam {t = unitrec _ _ _ _ _} ()
wk-lam {t = ℕ} ()
wk-lam {t = zero} ()
wk-lam {t = suc _} ()
wk-lam {t = natrec _ _ _ _ _ _ _} ()
wk-lam {t = Id _ _ _} ()
wk-lam {t = rfl} ()
wk-lam {t = J _ _ _ _ _ _ _ _} ()
wk-lam {t = K _ _ _ _ _ _} ()
wk-lam {t = []-cong _ _ _ _ _ _} ()
subst-lam :
t [ σ ] ≡ lam p u →
(∃ λ x → t ≡ var x) ⊎
∃ λ u′ → t ≡ lam p u′ × u′ [ liftSubst σ ] ≡ u
subst-lam {t = var x} _ = inj₁ (_ , refl)
subst-lam {t = lam _ _} refl = inj₂ (_ , refl , refl)
subst-lam {t = defn _} ()
subst-lam {t = Level} ()
subst-lam {t = zeroᵘ} ()
subst-lam {t = sucᵘ _} ()
subst-lam {t = _ supᵘ _} ()
subst-lam {t = U _} ()
subst-lam {t = Lift _ _} ()
subst-lam {t = lift _} ()
subst-lam {t = lower _} ()
subst-lam {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-lam {t = _ ∘⟨ _ ⟩ _} ()
subst-lam {t = prod _ _ _ _} ()
subst-lam {t = fst _ _} ()
subst-lam {t = snd _ _} ()
subst-lam {t = prodrec _ _ _ _ _ _} ()
subst-lam {t = Empty} ()
subst-lam {t = emptyrec _ _ _} ()
subst-lam {t = Unit _} ()
subst-lam {t = star _} ()
subst-lam {t = unitrec _ _ _ _ _} ()
subst-lam {t = ℕ} ()
subst-lam {t = zero} ()
subst-lam {t = suc _} ()
subst-lam {t = natrec _ _ _ _ _ _ _} ()
subst-lam {t = Id _ _ _} ()
subst-lam {t = rfl} ()
subst-lam {t = J _ _ _ _ _ _ _ _} ()
subst-lam {t = K _ _ _ _ _ _} ()
subst-lam {t = []-cong _ _ _ _ _ _} ()
wk-∘ :
wk ρ t ≡ u ∘⟨ p ⟩ v →
∃₂ λ u′ v′ → t ≡ u′ ∘⟨ p ⟩ v′ × wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-∘ {t = _ ∘⟨ _ ⟩ _} refl = _ , _ , refl , refl , refl
wk-∘ {t = var _} ()
wk-∘ {t = defn _} ()
wk-∘ {t = Level} ()
wk-∘ {t = zeroᵘ} ()
wk-∘ {t = sucᵘ _} ()
wk-∘ {t = _ supᵘ _} ()
wk-∘ {t = U _} ()
wk-∘ {t = Lift _ _} ()
wk-∘ {t = lift _} ()
wk-∘ {t = lower _} ()
wk-∘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-∘ {t = lam _ _} ()
wk-∘ {t = prod _ _ _ _} ()
wk-∘ {t = fst _ _} ()
wk-∘ {t = snd _ _} ()
wk-∘ {t = prodrec _ _ _ _ _ _} ()
wk-∘ {t = Empty} ()
wk-∘ {t = emptyrec _ _ _} ()
wk-∘ {t = Unit _} ()
wk-∘ {t = star _} ()
wk-∘ {t = unitrec _ _ _ _ _} ()
wk-∘ {t = ℕ} ()
wk-∘ {t = zero} ()
wk-∘ {t = suc _} ()
wk-∘ {t = natrec _ _ _ _ _ _ _} ()
wk-∘ {t = Id _ _ _} ()
wk-∘ {t = rfl} ()
wk-∘ {t = J _ _ _ _ _ _ _ _} ()
wk-∘ {t = K _ _ _ _ _ _} ()
wk-∘ {t = []-cong _ _ _ _ _ _} ()
subst-∘ :
t [ σ ] ≡ u ∘⟨ p ⟩ v →
(∃ λ x → t ≡ var x) ⊎
∃₂ λ u′ v′ → t ≡ u′ ∘⟨ p ⟩ v′ × u′ [ σ ] ≡ u × v′ [ σ ] ≡ v
subst-∘ {t = var x} _ = inj₁ (_ , refl)
subst-∘ {t = _ ∘ _} refl =
inj₂ (_ , _ , refl , refl , refl)
subst-∘ {t = defn _} ()
subst-∘ {t = Level} ()
subst-∘ {t = zeroᵘ} ()
subst-∘ {t = sucᵘ _} ()
subst-∘ {t = _ supᵘ _} ()
subst-∘ {t = U _} ()
subst-∘ {t = Lift _ _} ()
subst-∘ {t = lift _} ()
subst-∘ {t = lower _} ()
subst-∘ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-∘ {t = lam _ _} ()
subst-∘ {t = prod _ _ _ _} ()
subst-∘ {t = fst _ _} ()
subst-∘ {t = snd _ _} ()
subst-∘ {t = prodrec _ _ _ _ _ _} ()
subst-∘ {t = Empty} ()
subst-∘ {t = emptyrec _ _ _} ()
subst-∘ {t = Unit _} ()
subst-∘ {t = star _} ()
subst-∘ {t = unitrec _ _ _ _ _} ()
subst-∘ {t = ℕ} ()
subst-∘ {t = zero} ()
subst-∘ {t = suc _} ()
subst-∘ {t = natrec _ _ _ _ _ _ _} ()
subst-∘ {t = Id _ _ _} ()
subst-∘ {t = rfl} ()
subst-∘ {t = J _ _ _ _ _ _ _ _} ()
subst-∘ {t = K _ _ _ _ _ _} ()
subst-∘ {t = []-cong _ _ _ _ _ _} ()
wk-prod :
wk ρ t ≡ prod s p u v →
∃₂ λ u′ v′ → t ≡ prod s p u′ v′ × wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-prod {t = prod _ _ _ _} refl = _ , _ , refl , refl , refl
wk-prod {t = var _} ()
wk-prod {t = defn _} ()
wk-prod {t = Level} ()
wk-prod {t = zeroᵘ} ()
wk-prod {t = sucᵘ _} ()
wk-prod {t = _ supᵘ _} ()
wk-prod {t = U _} ()
wk-prod {t = Lift _ _} ()
wk-prod {t = lift _} ()
wk-prod {t = lower _} ()
wk-prod {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-prod {t = lam _ _} ()
wk-prod {t = _ ∘⟨ _ ⟩ _} ()
wk-prod {t = fst _ _} ()
wk-prod {t = snd _ _} ()
wk-prod {t = prodrec _ _ _ _ _ _} ()
wk-prod {t = Empty} ()
wk-prod {t = emptyrec _ _ _} ()
wk-prod {t = Unit _} ()
wk-prod {t = star _} ()
wk-prod {t = unitrec _ _ _ _ _} ()
wk-prod {t = ℕ} ()
wk-prod {t = zero} ()
wk-prod {t = suc _} ()
wk-prod {t = natrec _ _ _ _ _ _ _} ()
wk-prod {t = Id _ _ _} ()
wk-prod {t = rfl} ()
wk-prod {t = J _ _ _ _ _ _ _ _} ()
wk-prod {t = K _ _ _ _ _ _} ()
wk-prod {t = []-cong _ _ _ _ _ _} ()
subst-prod :
t [ σ ] ≡ prod s p u v →
(∃ λ x → t ≡ var x) ⊎
∃₂ λ u′ v′ → t ≡ prod s p u′ v′ × u′ [ σ ] ≡ u × v′ [ σ ] ≡ v
subst-prod {t = var _} _ =
inj₁ (_ , refl)
subst-prod {t = prod _ _ _ _} refl =
inj₂ (_ , _ , refl , refl , refl)
subst-prod {t = defn _} ()
subst-prod {t = Level} ()
subst-prod {t = zeroᵘ} ()
subst-prod {t = sucᵘ _} ()
subst-prod {t = _ supᵘ _} ()
subst-prod {t = U _} ()
subst-prod {t = Lift _ _} ()
subst-prod {t = lift _} ()
subst-prod {t = lower _} ()
subst-prod {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-prod {t = lam _ _} ()
subst-prod {t = _ ∘⟨ _ ⟩ _} ()
subst-prod {t = fst _ _} ()
subst-prod {t = snd _ _} ()
subst-prod {t = prodrec _ _ _ _ _ _} ()
subst-prod {t = Empty} ()
subst-prod {t = emptyrec _ _ _} ()
subst-prod {t = Unit _} ()
subst-prod {t = star _} ()
subst-prod {t = unitrec _ _ _ _ _} ()
subst-prod {t = ℕ} ()
subst-prod {t = zero} ()
subst-prod {t = suc _} ()
subst-prod {t = natrec _ _ _ _ _ _ _} ()
subst-prod {t = Id _ _ _} ()
subst-prod {t = rfl} ()
subst-prod {t = J _ _ _ _ _ _ _ _} ()
subst-prod {t = K _ _ _ _ _ _} ()
subst-prod {t = []-cong _ _ _ _ _ _} ()
wk-fst :
wk ρ t ≡ fst p u →
∃ λ u′ → t ≡ fst p u′ × wk ρ u′ ≡ u
wk-fst {t = fst _ _} refl = _ , refl , refl
wk-fst {t = var _} ()
wk-fst {t = defn _} ()
wk-fst {t = Level} ()
wk-fst {t = zeroᵘ} ()
wk-fst {t = sucᵘ _} ()
wk-fst {t = _ supᵘ _} ()
wk-fst {t = U _} ()
wk-fst {t = Lift _ _} ()
wk-fst {t = lift _} ()
wk-fst {t = lower _} ()
wk-fst {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-fst {t = lam _ _} ()
wk-fst {t = _ ∘⟨ _ ⟩ _} ()
wk-fst {t = prod _ _ _ _} ()
wk-fst {t = snd _ _} ()
wk-fst {t = prodrec _ _ _ _ _ _} ()
wk-fst {t = Empty} ()
wk-fst {t = emptyrec _ _ _} ()
wk-fst {t = Unit _} ()
wk-fst {t = star _} ()
wk-fst {t = unitrec _ _ _ _ _} ()
wk-fst {t = ℕ} ()
wk-fst {t = zero} ()
wk-fst {t = suc _} ()
wk-fst {t = natrec _ _ _ _ _ _ _} ()
wk-fst {t = Id _ _ _} ()
wk-fst {t = rfl} ()
wk-fst {t = J _ _ _ _ _ _ _ _} ()
wk-fst {t = K _ _ _ _ _ _} ()
wk-fst {t = []-cong _ _ _ _ _ _} ()
subst-fst :
t [ σ ] ≡ fst p u →
(∃ λ x → t ≡ var x) ⊎
∃ λ u′ → t ≡ fst p u′ × u′ [ σ ] ≡ u
subst-fst {t = var _} _ = inj₁ (_ , refl)
subst-fst {t = fst _ _} refl = inj₂ (_ , refl , refl)
subst-fst {t = defn _} ()
subst-fst {t = Level} ()
subst-fst {t = zeroᵘ} ()
subst-fst {t = sucᵘ _} ()
subst-fst {t = _ supᵘ _} ()
subst-fst {t = U _} ()
subst-fst {t = Lift _ _} ()
subst-fst {t = lift _} ()
subst-fst {t = lower _} ()
subst-fst {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-fst {t = lam _ _} ()
subst-fst {t = _ ∘⟨ _ ⟩ _} ()
subst-fst {t = prod _ _ _ _} ()
subst-fst {t = snd _ _} ()
subst-fst {t = prodrec _ _ _ _ _ _} ()
subst-fst {t = Empty} ()
subst-fst {t = emptyrec _ _ _} ()
subst-fst {t = Unit _} ()
subst-fst {t = star _} ()
subst-fst {t = unitrec _ _ _ _ _} ()
subst-fst {t = ℕ} ()
subst-fst {t = zero} ()
subst-fst {t = suc _} ()
subst-fst {t = natrec _ _ _ _ _ _ _} ()
subst-fst {t = Id _ _ _} ()
subst-fst {t = rfl} ()
subst-fst {t = J _ _ _ _ _ _ _ _} ()
subst-fst {t = K _ _ _ _ _ _} ()
subst-fst {t = []-cong _ _ _ _ _ _} ()
wk-snd :
wk ρ t ≡ snd p u →
∃ λ u′ → t ≡ snd p u′ × wk ρ u′ ≡ u
wk-snd {t = snd _ _} refl = _ , refl , refl
wk-snd {t = var _} ()
wk-snd {t = defn _} ()
wk-snd {t = Level} ()
wk-snd {t = zeroᵘ} ()
wk-snd {t = sucᵘ _} ()
wk-snd {t = _ supᵘ _} ()
wk-snd {t = U _} ()
wk-snd {t = Lift _ _} ()
wk-snd {t = lift _} ()
wk-snd {t = lower _} ()
wk-snd {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-snd {t = lam _ _} ()
wk-snd {t = _ ∘⟨ _ ⟩ _} ()
wk-snd {t = prod _ _ _ _} ()
wk-snd {t = fst _ _} ()
wk-snd {t = prodrec _ _ _ _ _ _} ()
wk-snd {t = Empty} ()
wk-snd {t = emptyrec _ _ _} ()
wk-snd {t = Unit _} ()
wk-snd {t = star _} ()
wk-snd {t = unitrec _ _ _ _ _} ()
wk-snd {t = ℕ} ()
wk-snd {t = zero} ()
wk-snd {t = suc _} ()
wk-snd {t = natrec _ _ _ _ _ _ _} ()
wk-snd {t = Id _ _ _} ()
wk-snd {t = rfl} ()
wk-snd {t = J _ _ _ _ _ _ _ _} ()
wk-snd {t = K _ _ _ _ _ _} ()
wk-snd {t = []-cong _ _ _ _ _ _} ()
subst-snd :
t [ σ ] ≡ snd p u →
(∃ λ x → t ≡ var x) ⊎
∃ λ u′ → t ≡ snd p u′ × u′ [ σ ] ≡ u
subst-snd {t = var _} _ = inj₁ (_ , refl)
subst-snd {t = snd _ _} refl = inj₂ (_ , refl , refl)
subst-snd {t = defn _} ()
subst-snd {t = Level} ()
subst-snd {t = zeroᵘ} ()
subst-snd {t = sucᵘ _} ()
subst-snd {t = _ supᵘ _} ()
subst-snd {t = U _} ()
subst-snd {t = Lift _ _} ()
subst-snd {t = lift _} ()
subst-snd {t = lower _} ()
subst-snd {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-snd {t = lam _ _} ()
subst-snd {t = _ ∘⟨ _ ⟩ _} ()
subst-snd {t = prod _ _ _ _} ()
subst-snd {t = fst _ _} ()
subst-snd {t = prodrec _ _ _ _ _ _} ()
subst-snd {t = Empty} ()
subst-snd {t = emptyrec _ _ _} ()
subst-snd {t = Unit _} ()
subst-snd {t = star _} ()
subst-snd {t = unitrec _ _ _ _ _} ()
subst-snd {t = ℕ} ()
subst-snd {t = zero} ()
subst-snd {t = suc _} ()
subst-snd {t = natrec _ _ _ _ _ _ _} ()
subst-snd {t = Id _ _ _} ()
subst-snd {t = rfl} ()
subst-snd {t = J _ _ _ _ _ _ _ _} ()
subst-snd {t = K _ _ _ _ _ _} ()
subst-snd {t = []-cong _ _ _ _ _ _} ()
wk-prodrec :
wk ρ t ≡ prodrec r p q A u v →
∃₃ λ A′ u′ v′ →
t ≡ prodrec r p q A′ u′ v′ ×
wk (lift ρ) A′ ≡ A × wk ρ u′ ≡ u × wk (lift (lift ρ)) v′ ≡ v
wk-prodrec {t = prodrec _ _ _ _ _ _} refl =
_ , _ , _ , refl , refl , refl , refl
wk-prodrec {t = var _} ()
wk-prodrec {t = defn _} ()
wk-prodrec {t = Level} ()
wk-prodrec {t = zeroᵘ} ()
wk-prodrec {t = sucᵘ _} ()
wk-prodrec {t = _ supᵘ _} ()
wk-prodrec {t = U _} ()
wk-prodrec {t = Lift _ _} ()
wk-prodrec {t = lift _} ()
wk-prodrec {t = lower _} ()
wk-prodrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-prodrec {t = lam _ _} ()
wk-prodrec {t = _ ∘⟨ _ ⟩ _} ()
wk-prodrec {t = prod _ _ _ _} ()
wk-prodrec {t = fst _ _} ()
wk-prodrec {t = snd _ _} ()
wk-prodrec {t = Empty} ()
wk-prodrec {t = emptyrec _ _ _} ()
wk-prodrec {t = Unit _} ()
wk-prodrec {t = star _} ()
wk-prodrec {t = unitrec _ _ _ _ _} ()
wk-prodrec {t = ℕ} ()
wk-prodrec {t = zero} ()
wk-prodrec {t = suc _} ()
wk-prodrec {t = natrec _ _ _ _ _ _ _} ()
wk-prodrec {t = Id _ _ _} ()
wk-prodrec {t = rfl} ()
wk-prodrec {t = J _ _ _ _ _ _ _ _} ()
wk-prodrec {t = K _ _ _ _ _ _} ()
wk-prodrec {t = []-cong _ _ _ _ _ _} ()
subst-prodrec :
t [ σ ] ≡ prodrec r p q A u v →
(∃ λ x → t ≡ var x) ⊎
∃₃ λ A′ u′ v′ →
t ≡ prodrec r p q A′ u′ v′ ×
A′ [ liftSubst σ ] ≡ A × u′ [ σ ] ≡ u × v′ [ liftSubstn σ 2 ] ≡ v
subst-prodrec {t = var _} _ =
inj₁ (_ , refl)
subst-prodrec {t = prodrec _ _ _ _ _ _} refl =
inj₂ (_ , _ , _ , refl , refl , refl , refl)
subst-prodrec {t = defn _} ()
subst-prodrec {t = U _} ()
subst-prodrec {t = Level} ()
subst-prodrec {t = zeroᵘ} ()
subst-prodrec {t = sucᵘ _} ()
subst-prodrec {t = _ supᵘ _} ()
subst-prodrec {t = Lift _ _} ()
subst-prodrec {t = lift _} ()
subst-prodrec {t = lower _} ()
subst-prodrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-prodrec {t = lam _ _} ()
subst-prodrec {t = _ ∘⟨ _ ⟩ _} ()
subst-prodrec {t = prod _ _ _ _} ()
subst-prodrec {t = fst _ _} ()
subst-prodrec {t = snd _ _} ()
subst-prodrec {t = Empty} ()
subst-prodrec {t = emptyrec _ _ _} ()
subst-prodrec {t = Unit _} ()
subst-prodrec {t = star _} ()
subst-prodrec {t = unitrec _ _ _ _ _} ()
subst-prodrec {t = ℕ} ()
subst-prodrec {t = zero} ()
subst-prodrec {t = suc _} ()
subst-prodrec {t = natrec _ _ _ _ _ _ _} ()
subst-prodrec {t = Id _ _ _} ()
subst-prodrec {t = rfl} ()
subst-prodrec {t = J _ _ _ _ _ _ _ _} ()
subst-prodrec {t = K _ _ _ _ _ _} ()
subst-prodrec {t = []-cong _ _ _ _ _ _} ()
wk-Unit : wk ρ t ≡ Unit s → t ≡ Unit s
wk-Unit {t = Unit!} refl = refl
wk-Unit {t = var _} ()
wk-Unit {t = defn _} ()
wk-Unit {t = U _} ()
wk-Unit {t = Level} ()
wk-Unit {t = zeroᵘ} ()
wk-Unit {t = sucᵘ _} ()
wk-Unit {t = _ supᵘ _} ()
wk-Unit {t = Lift _ _} ()
wk-Unit {t = lift _} ()
wk-Unit {t = lower _} ()
wk-Unit {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-Unit {t = lam _ _} ()
wk-Unit {t = _ ∘⟨ _ ⟩ _} ()
wk-Unit {t = prod _ _ _ _} ()
wk-Unit {t = fst _ _} ()
wk-Unit {t = snd _ _} ()
wk-Unit {t = prodrec _ _ _ _ _ _} ()
wk-Unit {t = Empty} ()
wk-Unit {t = emptyrec _ _ _} ()
wk-Unit {t = star _} ()
wk-Unit {t = unitrec _ _ _ _ _} ()
wk-Unit {t = ℕ} ()
wk-Unit {t = zero} ()
wk-Unit {t = suc _} ()
wk-Unit {t = natrec _ _ _ _ _ _ _} ()
wk-Unit {t = Id _ _ _} ()
wk-Unit {t = rfl} ()
wk-Unit {t = J _ _ _ _ _ _ _ _} ()
wk-Unit {t = K _ _ _ _ _ _} ()
wk-Unit {t = []-cong _ _ _ _ _ _} ()
subst-Unit : t [ σ ] ≡ Unit s →
(∃ λ x → t ≡ var x) ⊎ t ≡ Unit s
subst-Unit {t = var _} _ = inj₁ (_ , refl)
subst-Unit {t = Unit!} refl = inj₂ refl
subst-Unit {t = defn _} ()
subst-Unit {t = U _} ()
subst-Unit {t = Level} ()
subst-Unit {t = zeroᵘ} ()
subst-Unit {t = sucᵘ _} ()
subst-Unit {t = _ supᵘ _} ()
subst-Unit {t = Lift _ _} ()
subst-Unit {t = lift _} ()
subst-Unit {t = lower _} ()
subst-Unit {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-Unit {t = lam _ _} ()
subst-Unit {t = _ ∘⟨ _ ⟩ _} ()
subst-Unit {t = prod _ _ _ _} ()
subst-Unit {t = fst _ _} ()
subst-Unit {t = snd _ _} ()
subst-Unit {t = prodrec _ _ _ _ _ _} ()
subst-Unit {t = Empty} ()
subst-Unit {t = emptyrec _ _ _} ()
subst-Unit {t = star _} ()
subst-Unit {t = unitrec _ _ _ _ _} ()
subst-Unit {t = ℕ} ()
subst-Unit {t = zero} ()
subst-Unit {t = suc _} ()
subst-Unit {t = natrec _ _ _ _ _ _ _} ()
subst-Unit {t = Id _ _ _} ()
subst-Unit {t = rfl} ()
subst-Unit {t = J _ _ _ _ _ _ _ _} ()
subst-Unit {t = K _ _ _ _ _ _} ()
subst-Unit {t = []-cong _ _ _ _ _ _} ()
wk-star : wk ρ t ≡ star s → t ≡ star s
wk-star {t = star!} refl = refl
wk-star {t = var _} ()
wk-star {t = defn _} ()
wk-star {t = U _} ()
wk-star {t = Level} ()
wk-star {t = zeroᵘ} ()
wk-star {t = sucᵘ _} ()
wk-star {t = _ supᵘ _} ()
wk-star {t = Lift _ _} ()
wk-star {t = lift _} ()
wk-star {t = lower _} ()
wk-star {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-star {t = lam _ _} ()
wk-star {t = _ ∘⟨ _ ⟩ _} ()
wk-star {t = prod _ _ _ _} ()
wk-star {t = fst _ _} ()
wk-star {t = snd _ _} ()
wk-star {t = prodrec _ _ _ _ _ _} ()
wk-star {t = Empty} ()
wk-star {t = emptyrec _ _ _} ()
wk-star {t = Unit _} ()
wk-star {t = unitrec _ _ _ _ _} ()
wk-star {t = ℕ} ()
wk-star {t = zero} ()
wk-star {t = suc _} ()
wk-star {t = natrec _ _ _ _ _ _ _} ()
wk-star {t = Id _ _ _} ()
wk-star {t = rfl} ()
wk-star {t = J _ _ _ _ _ _ _ _} ()
wk-star {t = K _ _ _ _ _ _} ()
wk-star {t = []-cong _ _ _ _ _ _} ()
subst-star : t [ σ ] ≡ star s →
(∃ λ x → t ≡ var x) ⊎ t ≡ star s
subst-star {t = var _} _ = inj₁ (_ , refl)
subst-star {t = star!} refl = inj₂ refl
subst-star {t = defn _} ()
subst-star {t = U _} ()
subst-star {t = Level} ()
subst-star {t = zeroᵘ} ()
subst-star {t = sucᵘ _} ()
subst-star {t = _ supᵘ _} ()
subst-star {t = Lift _ _} ()
subst-star {t = lift _} ()
subst-star {t = lower _} ()
subst-star {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-star {t = lam _ _} ()
subst-star {t = _ ∘⟨ _ ⟩ _} ()
subst-star {t = prod _ _ _ _} ()
subst-star {t = fst _ _} ()
subst-star {t = snd _ _} ()
subst-star {t = prodrec _ _ _ _ _ _} ()
subst-star {t = Empty} ()
subst-star {t = emptyrec _ _ _} ()
subst-star {t = Unit _} ()
subst-star {t = unitrec _ _ _ _ _} ()
subst-star {t = ℕ} ()
subst-star {t = zero} ()
subst-star {t = suc _} ()
subst-star {t = natrec _ _ _ _ _ _ _} ()
subst-star {t = Id _ _ _} ()
subst-star {t = rfl} ()
subst-star {t = J _ _ _ _ _ _ _ _} ()
subst-star {t = K _ _ _ _ _ _} ()
subst-star {t = []-cong _ _ _ _ _ _} ()
wk-unitrec :
wk ρ t ≡ unitrec p q A u v →
∃₃ λ A′ u′ v′ →
t ≡ unitrec p q A′ u′ v′ ×
wk (lift ρ) A′ ≡ A × wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-unitrec {t = unitrec _ _ _ _ _} refl =
_ , _ , _ , refl , refl , refl , refl
wk-unitrec {t = var _} ()
wk-unitrec {t = defn _} ()
wk-unitrec {t = U _} ()
wk-unitrec {t = Level} ()
wk-unitrec {t = zeroᵘ} ()
wk-unitrec {t = sucᵘ _} ()
wk-unitrec {t = _ supᵘ _} ()
wk-unitrec {t = Lift _ _} ()
wk-unitrec {t = lift _} ()
wk-unitrec {t = lower _} ()
wk-unitrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-unitrec {t = lam _ _} ()
wk-unitrec {t = _ ∘⟨ _ ⟩ _} ()
wk-unitrec {t = prod _ _ _ _} ()
wk-unitrec {t = fst _ _} ()
wk-unitrec {t = snd _ _} ()
wk-unitrec {t = prodrec _ _ _ _ _ _} ()
wk-unitrec {t = Empty} ()
wk-unitrec {t = emptyrec _ _ _} ()
wk-unitrec {t = Unit _} ()
wk-unitrec {t = star _} ()
wk-unitrec {t = ℕ} ()
wk-unitrec {t = zero} ()
wk-unitrec {t = suc _} ()
wk-unitrec {t = natrec _ _ _ _ _ _ _} ()
wk-unitrec {t = Id _ _ _} ()
wk-unitrec {t = rfl} ()
wk-unitrec {t = J _ _ _ _ _ _ _ _} ()
wk-unitrec {t = K _ _ _ _ _ _} ()
wk-unitrec {t = []-cong _ _ _ _ _ _} ()
subst-unitrec :
t [ σ ] ≡ unitrec p q A u v →
(∃ λ x → t ≡ var x) ⊎
∃₃ λ A′ u′ v′ →
t ≡ unitrec p q A′ u′ v′ ×
A′ [ liftSubst σ ] ≡ A × u′ [ σ ] ≡ u × v′ [ σ ] ≡ v
subst-unitrec {t = var _} _ =
inj₁ (_ , refl)
subst-unitrec {t = unitrec _ _ _ _ _} refl =
inj₂ (_ , _ , _ , refl , refl , refl , refl)
subst-unitrec {t = defn _} ()
subst-unitrec {t = Level} ()
subst-unitrec {t = zeroᵘ} ()
subst-unitrec {t = sucᵘ _} ()
subst-unitrec {t = _ supᵘ _} ()
subst-unitrec {t = U _} ()
subst-unitrec {t = Lift _ _} ()
subst-unitrec {t = lift _} ()
subst-unitrec {t = lower _} ()
subst-unitrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-unitrec {t = lam _ _} ()
subst-unitrec {t = _ ∘⟨ _ ⟩ _} ()
subst-unitrec {t = prod _ _ _ _} ()
subst-unitrec {t = fst _ _} ()
subst-unitrec {t = snd _ _} ()
subst-unitrec {t = prodrec _ _ _ _ _ _} ()
subst-unitrec {t = Empty} ()
subst-unitrec {t = emptyrec _ _ _} ()
subst-unitrec {t = Unit _} ()
subst-unitrec {t = star _} ()
subst-unitrec {t = ℕ} ()
subst-unitrec {t = zero} ()
subst-unitrec {t = suc _} ()
subst-unitrec {t = natrec _ _ _ _ _ _ _} ()
subst-unitrec {t = Id _ _ _} ()
subst-unitrec {t = rfl} ()
subst-unitrec {t = J _ _ _ _ _ _ _ _} ()
subst-unitrec {t = K _ _ _ _ _ _} ()
subst-unitrec {t = []-cong _ _ _ _ _ _} ()
wk-Empty : wk ρ t ≡ Empty → t ≡ Empty
wk-Empty {t = Empty} refl = refl
wk-Empty {t = var _} ()
wk-Empty {t = defn _} ()
wk-Empty {t = U _} ()
wk-Empty {t = Level} ()
wk-Empty {t = zeroᵘ} ()
wk-Empty {t = sucᵘ _} ()
wk-Empty {t = _ supᵘ _} ()
wk-Empty {t = Lift _ _} ()
wk-Empty {t = lift _} ()
wk-Empty {t = lower _} ()
wk-Empty {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-Empty {t = lam _ _} ()
wk-Empty {t = _ ∘⟨ _ ⟩ _} ()
wk-Empty {t = prod _ _ _ _} ()
wk-Empty {t = fst _ _} ()
wk-Empty {t = snd _ _} ()
wk-Empty {t = prodrec _ _ _ _ _ _} ()
wk-Empty {t = emptyrec _ _ _} ()
wk-Empty {t = Unit _} ()
wk-Empty {t = star _} ()
wk-Empty {t = unitrec _ _ _ _ _} ()
wk-Empty {t = ℕ} ()
wk-Empty {t = zero} ()
wk-Empty {t = suc _} ()
wk-Empty {t = natrec _ _ _ _ _ _ _} ()
wk-Empty {t = Id _ _ _} ()
wk-Empty {t = rfl} ()
wk-Empty {t = J _ _ _ _ _ _ _ _} ()
wk-Empty {t = K _ _ _ _ _ _} ()
wk-Empty {t = []-cong _ _ _ _ _ _} ()
subst-Empty : t [ σ ] ≡ Empty →
(∃ λ x → t ≡ var x) ⊎ t ≡ Empty
subst-Empty {t = var _} _ = inj₁ (_ , refl)
subst-Empty {t = Empty} refl = inj₂ refl
subst-Empty {t = defn _} ()
subst-Empty {t = U _} ()
subst-Empty {t = Level} ()
subst-Empty {t = zeroᵘ} ()
subst-Empty {t = sucᵘ _} ()
subst-Empty {t = _ supᵘ _} ()
subst-Empty {t = Lift _ _} ()
subst-Empty {t = lift _} ()
subst-Empty {t = lower _} ()
subst-Empty {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-Empty {t = lam _ _} ()
subst-Empty {t = _ ∘⟨ _ ⟩ _} ()
subst-Empty {t = prod _ _ _ _} ()
subst-Empty {t = fst _ _} ()
subst-Empty {t = snd _ _} ()
subst-Empty {t = prodrec _ _ _ _ _ _} ()
subst-Empty {t = emptyrec _ _ _} ()
subst-Empty {t = Unit _} ()
subst-Empty {t = star _} ()
subst-Empty {t = unitrec _ _ _ _ _} ()
subst-Empty {t = ℕ} ()
subst-Empty {t = zero} ()
subst-Empty {t = suc _} ()
subst-Empty {t = natrec _ _ _ _ _ _ _} ()
subst-Empty {t = Id _ _ _} ()
subst-Empty {t = rfl} ()
subst-Empty {t = J _ _ _ _ _ _ _ _} ()
subst-Empty {t = K _ _ _ _ _ _} ()
subst-Empty {t = []-cong _ _ _ _ _ _} ()
wk-emptyrec :
wk ρ t ≡ emptyrec p A u →
∃₂ λ A′ u′ → t ≡ emptyrec p A′ u′ × wk ρ A′ ≡ A × wk ρ u′ ≡ u
wk-emptyrec {t = emptyrec _ _ _} refl =
_ , _ , refl , refl , refl
wk-emptyrec {t = var _} ()
wk-emptyrec {t = defn _} ()
wk-emptyrec {t = U _} ()
wk-emptyrec {t = Level} ()
wk-emptyrec {t = zeroᵘ} ()
wk-emptyrec {t = sucᵘ _} ()
wk-emptyrec {t = _ supᵘ _} ()
wk-emptyrec {t = Lift _ _} ()
wk-emptyrec {t = lift _} ()
wk-emptyrec {t = lower _} ()
wk-emptyrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-emptyrec {t = lam _ _} ()
wk-emptyrec {t = _ ∘⟨ _ ⟩ _} ()
wk-emptyrec {t = prod _ _ _ _} ()
wk-emptyrec {t = fst _ _} ()
wk-emptyrec {t = snd _ _} ()
wk-emptyrec {t = prodrec _ _ _ _ _ _} ()
wk-emptyrec {t = Empty} ()
wk-emptyrec {t = Unit _} ()
wk-emptyrec {t = star _} ()
wk-emptyrec {t = unitrec _ _ _ _ _} ()
wk-emptyrec {t = ℕ} ()
wk-emptyrec {t = zero} ()
wk-emptyrec {t = suc _} ()
wk-emptyrec {t = natrec _ _ _ _ _ _ _} ()
wk-emptyrec {t = Id _ _ _} ()
wk-emptyrec {t = rfl} ()
wk-emptyrec {t = J _ _ _ _ _ _ _ _} ()
wk-emptyrec {t = K _ _ _ _ _ _} ()
wk-emptyrec {t = []-cong _ _ _ _ _ _} ()
subst-emptyrec :
t [ σ ] ≡ emptyrec p A u →
(∃ λ x → t ≡ var x) ⊎
∃₂ λ A′ u′ → t ≡ emptyrec p A′ u′ × A′ [ σ ] ≡ A × u′ [ σ ] ≡ u
subst-emptyrec {t = var _} _ =
inj₁ (_ , refl)
subst-emptyrec {t = emptyrec _ _ _} refl =
inj₂ (_ , _ , refl , refl , refl)
subst-emptyrec {t = defn _} ()
subst-emptyrec {t = U _} ()
subst-emptyrec {t = Level} ()
subst-emptyrec {t = zeroᵘ} ()
subst-emptyrec {t = sucᵘ _} ()
subst-emptyrec {t = _ supᵘ _} ()
subst-emptyrec {t = Lift _ _} ()
subst-emptyrec {t = lift _} ()
subst-emptyrec {t = lower _} ()
subst-emptyrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-emptyrec {t = lam _ _} ()
subst-emptyrec {t = _ ∘⟨ _ ⟩ _} ()
subst-emptyrec {t = prod _ _ _ _} ()
subst-emptyrec {t = fst _ _} ()
subst-emptyrec {t = snd _ _} ()
subst-emptyrec {t = prodrec _ _ _ _ _ _} ()
subst-emptyrec {t = Empty} ()
subst-emptyrec {t = Unit _} ()
subst-emptyrec {t = star _} ()
subst-emptyrec {t = unitrec _ _ _ _ _} ()
subst-emptyrec {t = ℕ} ()
subst-emptyrec {t = zero} ()
subst-emptyrec {t = suc _} ()
subst-emptyrec {t = natrec _ _ _ _ _ _ _} ()
subst-emptyrec {t = Id _ _ _} ()
subst-emptyrec {t = rfl} ()
subst-emptyrec {t = J _ _ _ _ _ _ _ _} ()
subst-emptyrec {t = K _ _ _ _ _ _} ()
subst-emptyrec {t = []-cong _ _ _ _ _ _} ()
wk-ℕ : wk ρ t ≡ ℕ → t ≡ ℕ
wk-ℕ {t = ℕ} refl = refl
wk-ℕ {t = var _} ()
wk-ℕ {t = defn _} ()
wk-ℕ {t = U _} ()
wk-ℕ {t = Level} ()
wk-ℕ {t = zeroᵘ} ()
wk-ℕ {t = sucᵘ _} ()
wk-ℕ {t = _ supᵘ _} ()
wk-ℕ {t = Lift _ _} ()
wk-ℕ {t = lift _} ()
wk-ℕ {t = lower _} ()
wk-ℕ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-ℕ {t = lam _ _} ()
wk-ℕ {t = _ ∘⟨ _ ⟩ _} ()
wk-ℕ {t = prod _ _ _ _} ()
wk-ℕ {t = fst _ _} ()
wk-ℕ {t = snd _ _} ()
wk-ℕ {t = prodrec _ _ _ _ _ _} ()
wk-ℕ {t = Empty} ()
wk-ℕ {t = emptyrec _ _ _} ()
wk-ℕ {t = Unit _} ()
wk-ℕ {t = star _} ()
wk-ℕ {t = unitrec _ _ _ _ _} ()
wk-ℕ {t = zero} ()
wk-ℕ {t = suc _} ()
wk-ℕ {t = natrec _ _ _ _ _ _ _} ()
wk-ℕ {t = Id _ _ _} ()
wk-ℕ {t = rfl} ()
wk-ℕ {t = J _ _ _ _ _ _ _ _} ()
wk-ℕ {t = K _ _ _ _ _ _} ()
wk-ℕ {t = []-cong _ _ _ _ _ _} ()
subst-ℕ : t [ σ ] ≡ ℕ → (∃ λ x → t ≡ var x) ⊎ t ≡ ℕ
subst-ℕ {t = var _} _ = inj₁ (_ , refl)
subst-ℕ {t = ℕ} refl = inj₂ refl
subst-ℕ {t = defn _} ()
subst-ℕ {t = U _} ()
subst-ℕ {t = Level} ()
subst-ℕ {t = zeroᵘ} ()
subst-ℕ {t = sucᵘ _} ()
subst-ℕ {t = _ supᵘ _} ()
subst-ℕ {t = Lift _ _} ()
subst-ℕ {t = lift _} ()
subst-ℕ {t = lower _} ()
subst-ℕ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-ℕ {t = lam _ _} ()
subst-ℕ {t = _ ∘⟨ _ ⟩ _} ()
subst-ℕ {t = prod _ _ _ _} ()
subst-ℕ {t = fst _ _} ()
subst-ℕ {t = snd _ _} ()
subst-ℕ {t = prodrec _ _ _ _ _ _} ()
subst-ℕ {t = Empty} ()
subst-ℕ {t = emptyrec _ _ _} ()
subst-ℕ {t = Unit _} ()
subst-ℕ {t = star _} ()
subst-ℕ {t = unitrec _ _ _ _ _} ()
subst-ℕ {t = zero} ()
subst-ℕ {t = suc _} ()
subst-ℕ {t = natrec _ _ _ _ _ _ _} ()
subst-ℕ {t = Id _ _ _} ()
subst-ℕ {t = rfl} ()
subst-ℕ {t = J _ _ _ _ _ _ _ _} ()
subst-ℕ {t = K _ _ _ _ _ _} ()
subst-ℕ {t = []-cong _ _ _ _ _ _} ()
wk-zero : wk ρ t ≡ zero → t ≡ zero
wk-zero {t = zero} refl = refl
wk-zero {t = var _} ()
wk-zero {t = defn _} ()
wk-zero {t = U _} ()
wk-zero {t = Level} ()
wk-zero {t = zeroᵘ} ()
wk-zero {t = sucᵘ _} ()
wk-zero {t = _ supᵘ _} ()
wk-zero {t = Lift _ _} ()
wk-zero {t = lift _} ()
wk-zero {t = lower _} ()
wk-zero {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-zero {t = lam _ _} ()
wk-zero {t = _ ∘⟨ _ ⟩ _} ()
wk-zero {t = prod _ _ _ _} ()
wk-zero {t = fst _ _} ()
wk-zero {t = snd _ _} ()
wk-zero {t = prodrec _ _ _ _ _ _} ()
wk-zero {t = Empty} ()
wk-zero {t = emptyrec _ _ _} ()
wk-zero {t = Unit _} ()
wk-zero {t = star _} ()
wk-zero {t = unitrec _ _ _ _ _} ()
wk-zero {t = ℕ} ()
wk-zero {t = suc _} ()
wk-zero {t = natrec _ _ _ _ _ _ _} ()
wk-zero {t = Id _ _ _} ()
wk-zero {t = rfl} ()
wk-zero {t = J _ _ _ _ _ _ _ _} ()
wk-zero {t = K _ _ _ _ _ _} ()
wk-zero {t = []-cong _ _ _ _ _ _} ()
subst-zero : t [ σ ] ≡ zero → (∃ λ x → t ≡ var x) ⊎ t ≡ zero
subst-zero {t = var _} _ = inj₁ (_ , refl)
subst-zero {t = zero} refl = inj₂ refl
subst-zero {t = defn _} ()
subst-zero {t = U _} ()
subst-zero {t = Level} ()
subst-zero {t = zeroᵘ} ()
subst-zero {t = sucᵘ _} ()
subst-zero {t = _ supᵘ _} ()
subst-zero {t = Lift _ _} ()
subst-zero {t = lift _} ()
subst-zero {t = lower _} ()
subst-zero {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-zero {t = lam _ _} ()
subst-zero {t = _ ∘⟨ _ ⟩ _} ()
subst-zero {t = prod _ _ _ _} ()
subst-zero {t = fst _ _} ()
subst-zero {t = snd _ _} ()
subst-zero {t = prodrec _ _ _ _ _ _} ()
subst-zero {t = Empty} ()
subst-zero {t = emptyrec _ _ _} ()
subst-zero {t = Unit _} ()
subst-zero {t = star _} ()
subst-zero {t = unitrec _ _ _ _ _} ()
subst-zero {t = ℕ} ()
subst-zero {t = suc _} ()
subst-zero {t = natrec _ _ _ _ _ _ _} ()
subst-zero {t = Id _ _ _} ()
subst-zero {t = rfl} ()
subst-zero {t = J _ _ _ _ _ _ _ _} ()
subst-zero {t = K _ _ _ _ _ _} ()
subst-zero {t = []-cong _ _ _ _ _ _} ()
wk-suc :
wk ρ t ≡ suc u →
∃ λ u′ → t ≡ suc u′ × wk ρ u′ ≡ u
wk-suc {t = suc _} refl = _ , refl , refl
wk-suc {t = var _} ()
wk-suc {t = defn _} ()
wk-suc {t = U _} ()
wk-suc {t = Level} ()
wk-suc {t = zeroᵘ} ()
wk-suc {t = sucᵘ _} ()
wk-suc {t = _ supᵘ _} ()
wk-suc {t = Lift _ _} ()
wk-suc {t = lift _} ()
wk-suc {t = lower _} ()
wk-suc {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-suc {t = lam _ _} ()
wk-suc {t = _ ∘⟨ _ ⟩ _} ()
wk-suc {t = prod _ _ _ _} ()
wk-suc {t = fst _ _} ()
wk-suc {t = snd _ _} ()
wk-suc {t = prodrec _ _ _ _ _ _} ()
wk-suc {t = Empty} ()
wk-suc {t = emptyrec _ _ _} ()
wk-suc {t = Unit _} ()
wk-suc {t = star _} ()
wk-suc {t = unitrec _ _ _ _ _} ()
wk-suc {t = ℕ} ()
wk-suc {t = zero} ()
wk-suc {t = natrec _ _ _ _ _ _ _} ()
wk-suc {t = Id _ _ _} ()
wk-suc {t = rfl} ()
wk-suc {t = J _ _ _ _ _ _ _ _} ()
wk-suc {t = K _ _ _ _ _ _} ()
wk-suc {t = []-cong _ _ _ _ _ _} ()
subst-suc :
t [ σ ] ≡ suc u →
(∃ λ x → t ≡ var x) ⊎ ∃ λ u′ → t ≡ suc u′ × u′ [ σ ] ≡ u
subst-suc {t = var _} _ = inj₁ (_ , refl)
subst-suc {t = suc _} refl = inj₂ (_ , refl , refl)
subst-suc {t = defn _} ()
subst-suc {t = U _} ()
subst-suc {t = Level} ()
subst-suc {t = zeroᵘ} ()
subst-suc {t = sucᵘ _} ()
subst-suc {t = _ supᵘ _} ()
subst-suc {t = Lift _ _} ()
subst-suc {t = lift _} ()
subst-suc {t = lower _} ()
subst-suc {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-suc {t = lam _ _} ()
subst-suc {t = _ ∘⟨ _ ⟩ _} ()
subst-suc {t = prod _ _ _ _} ()
subst-suc {t = fst _ _} ()
subst-suc {t = snd _ _} ()
subst-suc {t = prodrec _ _ _ _ _ _} ()
subst-suc {t = Empty} ()
subst-suc {t = emptyrec _ _ _} ()
subst-suc {t = Unit _} ()
subst-suc {t = star _} ()
subst-suc {t = unitrec _ _ _ _ _} ()
subst-suc {t = ℕ} ()
subst-suc {t = zero} ()
subst-suc {t = natrec _ _ _ _ _ _ _} ()
subst-suc {t = Id _ _ _} ()
subst-suc {t = rfl} ()
subst-suc {t = J _ _ _ _ _ _ _ _} ()
subst-suc {t = K _ _ _ _ _ _} ()
subst-suc {t = []-cong _ _ _ _ _ _} ()
wk-natrec :
wk ρ t ≡ natrec p q r A u v w →
∃₄ λ A′ u′ v′ w′ →
t ≡ natrec p q r A′ u′ v′ w′ ×
wk (lift ρ) A′ ≡ A ×
wk ρ u′ ≡ u × wk (lift (lift ρ)) v′ ≡ v × wk ρ w′ ≡ w
wk-natrec {t = natrec _ _ _ _ _ _ _} refl =
_ , _ , _ , _ , refl , refl , refl , refl , refl
wk-natrec {t = var _} ()
wk-natrec {t = defn _} ()
wk-natrec {t = U _} ()
wk-natrec {t = Level} ()
wk-natrec {t = zeroᵘ} ()
wk-natrec {t = sucᵘ _} ()
wk-natrec {t = _ supᵘ _} ()
wk-natrec {t = Lift _ _} ()
wk-natrec {t = lift _} ()
wk-natrec {t = lower _} ()
wk-natrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-natrec {t = lam _ _} ()
wk-natrec {t = _ ∘⟨ _ ⟩ _} ()
wk-natrec {t = prod _ _ _ _} ()
wk-natrec {t = fst _ _} ()
wk-natrec {t = snd _ _} ()
wk-natrec {t = prodrec _ _ _ _ _ _} ()
wk-natrec {t = Empty} ()
wk-natrec {t = emptyrec _ _ _} ()
wk-natrec {t = Unit _} ()
wk-natrec {t = star _} ()
wk-natrec {t = unitrec _ _ _ _ _} ()
wk-natrec {t = ℕ} ()
wk-natrec {t = zero} ()
wk-natrec {t = suc _} ()
wk-natrec {t = Id _ _ _} ()
wk-natrec {t = rfl} ()
wk-natrec {t = J _ _ _ _ _ _ _ _} ()
wk-natrec {t = K _ _ _ _ _ _} ()
wk-natrec {t = []-cong _ _ _ _ _ _} ()
subst-natrec :
t [ σ ] ≡ natrec p q r A u v w →
(∃ λ x → t ≡ var x) ⊎
∃₄ λ A′ u′ v′ w′ →
t ≡ natrec p q r A′ u′ v′ w′ ×
A′ [ liftSubst σ ] ≡ A ×
u′ [ σ ] ≡ u × v′ [ liftSubstn σ 2 ] ≡ v × w′ [ σ ] ≡ w
subst-natrec {t = var _} _ =
inj₁ (_ , refl)
subst-natrec {t = natrec _ _ _ _ _ _ _} refl =
inj₂ (_ , _ , _ , _ , refl , refl , refl , refl , refl)
subst-natrec {t = defn _} ()
subst-natrec {t = U _} ()
subst-natrec {t = Level} ()
subst-natrec {t = zeroᵘ} ()
subst-natrec {t = sucᵘ _} ()
subst-natrec {t = _ supᵘ _} ()
subst-natrec {t = Lift _ _} ()
subst-natrec {t = lift _} ()
subst-natrec {t = lower _} ()
subst-natrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-natrec {t = lam _ _} ()
subst-natrec {t = _ ∘⟨ _ ⟩ _} ()
subst-natrec {t = prod _ _ _ _} ()
subst-natrec {t = fst _ _} ()
subst-natrec {t = snd _ _} ()
subst-natrec {t = prodrec _ _ _ _ _ _} ()
subst-natrec {t = Empty} ()
subst-natrec {t = emptyrec _ _ _} ()
subst-natrec {t = Unit _} ()
subst-natrec {t = star _} ()
subst-natrec {t = unitrec _ _ _ _ _} ()
subst-natrec {t = ℕ} ()
subst-natrec {t = zero} ()
subst-natrec {t = suc _} ()
subst-natrec {t = Id _ _ _} ()
subst-natrec {t = rfl} ()
subst-natrec {t = J _ _ _ _ _ _ _ _} ()
subst-natrec {t = K _ _ _ _ _ _} ()
subst-natrec {t = []-cong _ _ _ _ _ _} ()
wk-Id :
wk ρ v ≡ Id A t u →
∃₃ λ A′ t′ u′ →
v ≡ Id A′ t′ u′ ×
wk ρ A′ ≡ A × wk ρ t′ ≡ t × wk ρ u′ ≡ u
wk-Id {v = Id _ _ _} refl =
_ , _ , _ , refl , refl , refl , refl
wk-Id {v = var _} ()
wk-Id {v = defn _} ()
wk-Id {v = U _} ()
wk-Id {v = Level} ()
wk-Id {v = zeroᵘ} ()
wk-Id {v = sucᵘ _} ()
wk-Id {v = _ supᵘ _} ()
wk-Id {v = Lift _ _} ()
wk-Id {v = lift _} ()
wk-Id {v = lower _} ()
wk-Id {v = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-Id {v = lam _ _} ()
wk-Id {v = _ ∘⟨ _ ⟩ _} ()
wk-Id {v = prod _ _ _ _} ()
wk-Id {v = fst _ _} ()
wk-Id {v = snd _ _} ()
wk-Id {v = prodrec _ _ _ _ _ _} ()
wk-Id {v = Empty} ()
wk-Id {v = emptyrec _ _ _} ()
wk-Id {v = Unit _} ()
wk-Id {v = star _} ()
wk-Id {v = unitrec _ _ _ _ _} ()
wk-Id {v = ℕ} ()
wk-Id {v = zero} ()
wk-Id {v = suc _} ()
wk-Id {v = natrec _ _ _ _ _ _ _} ()
wk-Id {v = rfl} ()
wk-Id {v = J _ _ _ _ _ _ _ _} ()
wk-Id {v = K _ _ _ _ _ _} ()
wk-Id {v = []-cong _ _ _ _ _ _} ()
subst-Id :
v [ σ ] ≡ Id A t u →
(∃ λ x → v ≡ var x) ⊎
∃₃ λ A′ t′ u′ →
v ≡ Id A′ t′ u′ ×
A′ [ σ ] ≡ A × t′ [ σ ] ≡ t × u′ [ σ ] ≡ u
subst-Id {v = var _} _ =
inj₁ (_ , refl)
subst-Id {v = Id _ _ _} refl =
inj₂ (_ , _ , _ , refl , refl , refl , refl)
subst-Id {v = defn _} ()
subst-Id {v = U _} ()
subst-Id {v = Level} ()
subst-Id {v = zeroᵘ} ()
subst-Id {v = sucᵘ _} ()
subst-Id {v = _ supᵘ _} ()
subst-Id {v = Lift _ _} ()
subst-Id {v = lift _} ()
subst-Id {v = lower _} ()
subst-Id {v = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-Id {v = lam _ _} ()
subst-Id {v = _ ∘⟨ _ ⟩ _} ()
subst-Id {v = prod _ _ _ _} ()
subst-Id {v = fst _ _} ()
subst-Id {v = snd _ _} ()
subst-Id {v = prodrec _ _ _ _ _ _} ()
subst-Id {v = Empty} ()
subst-Id {v = emptyrec _ _ _} ()
subst-Id {v = Unit _} ()
subst-Id {v = star _} ()
subst-Id {v = unitrec _ _ _ _ _} ()
subst-Id {v = ℕ} ()
subst-Id {v = zero} ()
subst-Id {v = suc _} ()
subst-Id {v = natrec _ _ _ _ _ _ _} ()
subst-Id {v = rfl} ()
subst-Id {v = J _ _ _ _ _ _ _ _} ()
subst-Id {v = K _ _ _ _ _ _} ()
subst-Id {v = []-cong _ _ _ _ _ _} ()
wk-rfl : wk ρ t ≡ rfl → t ≡ rfl
wk-rfl {t = rfl} refl = refl
wk-rfl {t = var _} ()
wk-rfl {t = defn _} ()
wk-rfl {t = U _} ()
wk-rfl {t = Level} ()
wk-rfl {t = zeroᵘ} ()
wk-rfl {t = sucᵘ _} ()
wk-rfl {t = _ supᵘ _} ()
wk-rfl {t = Lift _ _} ()
wk-rfl {t = lift _} ()
wk-rfl {t = lower _} ()
wk-rfl {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-rfl {t = lam _ _} ()
wk-rfl {t = _ ∘⟨ _ ⟩ _} ()
wk-rfl {t = prod _ _ _ _} ()
wk-rfl {t = fst _ _} ()
wk-rfl {t = snd _ _} ()
wk-rfl {t = prodrec _ _ _ _ _ _} ()
wk-rfl {t = Empty} ()
wk-rfl {t = emptyrec _ _ _} ()
wk-rfl {t = Unit _} ()
wk-rfl {t = star _} ()
wk-rfl {t = unitrec _ _ _ _ _} ()
wk-rfl {t = ℕ} ()
wk-rfl {t = zero} ()
wk-rfl {t = suc _} ()
wk-rfl {t = natrec _ _ _ _ _ _ _} ()
wk-rfl {t = Id _ _ _} ()
wk-rfl {t = J _ _ _ _ _ _ _ _} ()
wk-rfl {t = K _ _ _ _ _ _} ()
wk-rfl {t = []-cong _ _ _ _ _ _} ()
subst-rfl : t [ σ ] ≡ rfl → (∃ λ x → t ≡ var x) ⊎ t ≡ rfl
subst-rfl {t = var x} _ = inj₁ (_ , refl)
subst-rfl {t = rfl} refl = inj₂ refl
subst-rfl {t = defn _} ()
subst-rfl {t = U _} ()
subst-rfl {t = Level} ()
subst-rfl {t = zeroᵘ} ()
subst-rfl {t = sucᵘ _} ()
subst-rfl {t = _ supᵘ _} ()
subst-rfl {t = Lift _ _} ()
subst-rfl {t = lift _} ()
subst-rfl {t = lower _} ()
subst-rfl {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-rfl {t = lam _ _} ()
subst-rfl {t = _ ∘⟨ _ ⟩ _} ()
subst-rfl {t = prod _ _ _ _} ()
subst-rfl {t = fst _ _} ()
subst-rfl {t = snd _ _} ()
subst-rfl {t = prodrec _ _ _ _ _ _} ()
subst-rfl {t = Empty} ()
subst-rfl {t = emptyrec _ _ _} ()
subst-rfl {t = Unit _} ()
subst-rfl {t = star _} ()
subst-rfl {t = unitrec _ _ _ _ _} ()
subst-rfl {t = ℕ} ()
subst-rfl {t = zero} ()
subst-rfl {t = suc _} ()
subst-rfl {t = natrec _ _ _ _ _ _ _} ()
subst-rfl {t = Id _ _ _} ()
subst-rfl {t = J _ _ _ _ _ _ _ _} ()
subst-rfl {t = K _ _ _ _ _ _} ()
subst-rfl {t = []-cong _ _ _ _ _ _} ()
wk-J :
wk ρ w ≡ J p q A t B u t′ v →
∃₆ λ A′ t″ B′ u′ t‴ v′ →
w ≡ J p q A′ t″ B′ u′ t‴ v′ ×
wk ρ A′ ≡ A × wk ρ t″ ≡ t × wk (lift (lift ρ)) B′ ≡ B ×
wk ρ u′ ≡ u × wk ρ t‴ ≡ t′ × wk ρ v′ ≡ v
wk-J {w = J _ _ _ _ _ _ _ _} refl =
_ , _ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl , refl
wk-J {w = var _} ()
wk-J {w = defn _} ()
wk-J {w = U _} ()
wk-J {w = Level} ()
wk-J {w = zeroᵘ} ()
wk-J {w = sucᵘ _} ()
wk-J {w = _ supᵘ _} ()
wk-J {w = Lift _ _} ()
wk-J {w = lift _} ()
wk-J {w = lower _} ()
wk-J {w = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-J {w = lam _ _} ()
wk-J {w = _ ∘⟨ _ ⟩ _} ()
wk-J {w = prod _ _ _ _} ()
wk-J {w = fst _ _} ()
wk-J {w = snd _ _} ()
wk-J {w = prodrec _ _ _ _ _ _} ()
wk-J {w = Empty} ()
wk-J {w = emptyrec _ _ _} ()
wk-J {w = Unit _} ()
wk-J {w = star _} ()
wk-J {w = unitrec _ _ _ _ _} ()
wk-J {w = ℕ} ()
wk-J {w = zero} ()
wk-J {w = suc _} ()
wk-J {w = natrec _ _ _ _ _ _ _} ()
wk-J {w = Id _ _ _} ()
wk-J {w = rfl} ()
wk-J {w = K _ _ _ _ _ _} ()
wk-J {w = []-cong _ _ _ _ _ _} ()
subst-J :
w [ σ ] ≡ J p q A t B u t′ v →
(∃ λ x → w ≡ var x) ⊎
∃₃ λ A′ t″ B′ → ∃₃ λ u′ t‴ v′ →
w ≡ J p q A′ t″ B′ u′ t‴ v′ ×
A′ [ σ ] ≡ A × t″ [ σ ] ≡ t × B′ [ liftSubstn σ 2 ] ≡ B ×
u′ [ σ ] ≡ u × t‴ [ σ ] ≡ t′ × v′ [ σ ] ≡ v
subst-J {w = var _} _ =
inj₁ (_ , refl)
subst-J {w = J _ _ _ _ _ _ _ _} refl =
inj₂ (_ , _ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl , refl)
subst-J {w = defn _} ()
subst-J {w = U _} ()
subst-J {w = Level} ()
subst-J {w = zeroᵘ} ()
subst-J {w = sucᵘ _} ()
subst-J {w = _ supᵘ _} ()
subst-J {w = Lift _ _} ()
subst-J {w = lift _} ()
subst-J {w = lower _} ()
subst-J {w = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-J {w = lam _ _} ()
subst-J {w = _ ∘⟨ _ ⟩ _} ()
subst-J {w = prod _ _ _ _} ()
subst-J {w = fst _ _} ()
subst-J {w = snd _ _} ()
subst-J {w = prodrec _ _ _ _ _ _} ()
subst-J {w = Empty} ()
subst-J {w = emptyrec _ _ _} ()
subst-J {w = Unit _} ()
subst-J {w = star _} ()
subst-J {w = unitrec _ _ _ _ _} ()
subst-J {w = ℕ} ()
subst-J {w = zero} ()
subst-J {w = suc _} ()
subst-J {w = natrec _ _ _ _ _ _ _} ()
subst-J {w = Id _ _ _} ()
subst-J {w = rfl} ()
subst-J {w = K _ _ _ _ _ _} ()
subst-J {w = []-cong _ _ _ _ _ _} ()
wk-K :
wk ρ w ≡ K p A t B u v →
∃₅ λ A′ t′ B′ u′ v′ →
w ≡ K p A′ t′ B′ u′ v′ ×
wk ρ A′ ≡ A × wk ρ t′ ≡ t × wk (lift ρ) B′ ≡ B ×
wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-K {w = K _ _ _ _ _ _} refl =
_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl
wk-K {w = var _} ()
wk-K {w = defn _} ()
wk-K {w = U _} ()
wk-K {w = Level} ()
wk-K {w = zeroᵘ} ()
wk-K {w = sucᵘ _} ()
wk-K {w = _ supᵘ _} ()
wk-K {w = Lift _ _} ()
wk-K {w = lift _} ()
wk-K {w = lower _} ()
wk-K {w = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-K {w = lam _ _} ()
wk-K {w = _ ∘⟨ _ ⟩ _} ()
wk-K {w = prod _ _ _ _} ()
wk-K {w = fst _ _} ()
wk-K {w = snd _ _} ()
wk-K {w = prodrec _ _ _ _ _ _} ()
wk-K {w = Empty} ()
wk-K {w = emptyrec _ _ _} ()
wk-K {w = Unit _} ()
wk-K {w = star _} ()
wk-K {w = unitrec _ _ _ _ _} ()
wk-K {w = ℕ} ()
wk-K {w = zero} ()
wk-K {w = suc _} ()
wk-K {w = natrec _ _ _ _ _ _ _} ()
wk-K {w = Id _ _ _} ()
wk-K {w = rfl} ()
wk-K {w = J _ _ _ _ _ _ _ _} ()
wk-K {w = []-cong _ _ _ _ _ _} ()
subst-K :
w [ σ ] ≡ K p A t B u v →
(∃ λ x → w ≡ var x) ⊎
∃₃ λ A′ t′ B′ → ∃₂ λ u′ v′ →
w ≡ K p A′ t′ B′ u′ v′ ×
A′ [ σ ] ≡ A × t′ [ σ ] ≡ t × B′ [ liftSubst σ ] ≡ B ×
u′ [ σ ] ≡ u × v′ [ σ ] ≡ v
subst-K {w = var _} _ =
inj₁ (_ , refl)
subst-K {w = K _ _ _ _ _ _} refl =
inj₂ (_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl)
subst-K {w = defn _} ()
subst-K {w = U _} ()
subst-K {w = Level} ()
subst-K {w = zeroᵘ} ()
subst-K {w = sucᵘ _} ()
subst-K {w = _ supᵘ _} ()
subst-K {w = Lift _ _} ()
subst-K {w = lift _} ()
subst-K {w = lower _} ()
subst-K {w = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-K {w = lam _ _} ()
subst-K {w = _ ∘⟨ _ ⟩ _} ()
subst-K {w = prod _ _ _ _} ()
subst-K {w = fst _ _} ()
subst-K {w = snd _ _} ()
subst-K {w = prodrec _ _ _ _ _ _} ()
subst-K {w = Empty} ()
subst-K {w = emptyrec _ _ _} ()
subst-K {w = Unit _} ()
subst-K {w = star _} ()
subst-K {w = unitrec _ _ _ _ _} ()
subst-K {w = ℕ} ()
subst-K {w = zero} ()
subst-K {w = suc _} ()
subst-K {w = natrec _ _ _ _ _ _ _} ()
subst-K {w = Id _ _ _} ()
subst-K {w = rfl} ()
subst-K {w = J _ _ _ _ _ _ _ _} ()
subst-K {w = []-cong _ _ _ _ _ _} ()
wk-[]-cong :
wk ρ w ≡ []-cong s l A t u v →
∃₅ λ l′ A′ t′ u′ v′ →
w ≡ []-cong s l′ A′ t′ u′ v′ ×
wk ρ l′ ≡ l × wk ρ A′ ≡ A × wk ρ t′ ≡ t × wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-[]-cong {w = []-cong _ _ _ _ _ _} refl =
_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl
wk-[]-cong {w = var _} ()
wk-[]-cong {w = defn _} ()
wk-[]-cong {w = U _} ()
wk-[]-cong {w = Level} ()
wk-[]-cong {w = zeroᵘ} ()
wk-[]-cong {w = sucᵘ _} ()
wk-[]-cong {w = _ supᵘ _} ()
wk-[]-cong {w = Lift _ _} ()
wk-[]-cong {w = lift _} ()
wk-[]-cong {w = lower _} ()
wk-[]-cong {w = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-[]-cong {w = lam _ _} ()
wk-[]-cong {w = _ ∘⟨ _ ⟩ _} ()
wk-[]-cong {w = prod _ _ _ _} ()
wk-[]-cong {w = fst _ _} ()
wk-[]-cong {w = snd _ _} ()
wk-[]-cong {w = prodrec _ _ _ _ _ _} ()
wk-[]-cong {w = Empty} ()
wk-[]-cong {w = emptyrec _ _ _} ()
wk-[]-cong {w = Unit _} ()
wk-[]-cong {w = star _} ()
wk-[]-cong {w = unitrec _ _ _ _ _} ()
wk-[]-cong {w = ℕ} ()
wk-[]-cong {w = zero} ()
wk-[]-cong {w = suc _} ()
wk-[]-cong {w = natrec _ _ _ _ _ _ _} ()
wk-[]-cong {w = Id _ _ _} ()
wk-[]-cong {w = rfl} ()
wk-[]-cong {w = J _ _ _ _ _ _ _ _} ()
wk-[]-cong {w = K _ _ _ _ _ _} ()
subst-[]-cong :
w [ σ ] ≡ []-cong s l A t u v →
(∃ λ x → w ≡ var x) ⊎
∃₅ λ l′ A′ t′ u′ v′ →
w ≡ []-cong s l′ A′ t′ u′ v′ ×
l′ [ σ ] ≡ l × A′ [ σ ] ≡ A × t′ [ σ ] ≡ t × u′ [ σ ] ≡ u ×
v′ [ σ ] ≡ v
subst-[]-cong {w = var _} _ =
inj₁ (_ , refl)
subst-[]-cong {w = []-cong _ _ _ _ _ _} refl =
inj₂ (_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl)
subst-[]-cong {w = defn _} ()
subst-[]-cong {w = U _} ()
subst-[]-cong {w = Level} ()
subst-[]-cong {w = zeroᵘ} ()
subst-[]-cong {w = sucᵘ _} ()
subst-[]-cong {w = _ supᵘ _} ()
subst-[]-cong {w = Lift _ _} ()
subst-[]-cong {w = lift _} ()
subst-[]-cong {w = lower _} ()
subst-[]-cong {w = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-[]-cong {w = lam _ _} ()
subst-[]-cong {w = _ ∘⟨ _ ⟩ _} ()
subst-[]-cong {w = prod _ _ _ _} ()
subst-[]-cong {w = fst _ _} ()
subst-[]-cong {w = snd _ _} ()
subst-[]-cong {w = prodrec _ _ _ _ _ _} ()
subst-[]-cong {w = Empty} ()
subst-[]-cong {w = emptyrec _ _ _} ()
subst-[]-cong {w = Unit _} ()
subst-[]-cong {w = star _} ()
subst-[]-cong {w = unitrec _ _ _ _ _} ()
subst-[]-cong {w = ℕ} ()
subst-[]-cong {w = zero} ()
subst-[]-cong {w = suc _} ()
subst-[]-cong {w = natrec _ _ _ _ _ _ _} ()
subst-[]-cong {w = Id _ _ _} ()
subst-[]-cong {w = rfl} ()
subst-[]-cong {w = J _ _ _ _ _ _ _ _} ()
subst-[]-cong {w = K _ _ _ _ _ _} ()