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
x : Fin _
α m : Nat
ρ : Wk _ _
A A₁ A₂ B l t t′ u u₁ u₂ u₃ 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 _ _ _ _ _ _} ()
wk-var {t = Quot _ _} ()
wk-var {t = class _} ()
wk-var {t = resp _ _ _ _ _} ()
wk-var {t = set _ _ _ _ _ _} ()
wk-var {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-var {t = Quot _ _} ()
subst-var {t = class _} ()
subst-var {t = resp _ _ _ _ _} ()
subst-var {t = set _ _ _ _ _ _} ()
subst-var {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-Level {t = Quot _ _} ()
wk-Level {t = class _} ()
wk-Level {t = resp _ _ _ _ _} ()
wk-Level {t = set _ _ _ _ _ _} ()
wk-Level {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-Level {t = Quot _ _} ()
subst-Level {t = class _} ()
subst-Level {t = resp _ _ _ _ _} ()
subst-Level {t = set _ _ _ _ _ _} ()
subst-Level {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-zeroᵘ {t = Quot _ _} ()
wk-zeroᵘ {t = class _} ()
wk-zeroᵘ {t = resp _ _ _ _ _} ()
wk-zeroᵘ {t = set _ _ _ _ _ _} ()
wk-zeroᵘ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-zeroᵘ {t = Quot _ _} ()
subst-zeroᵘ {t = class _} ()
subst-zeroᵘ {t = resp _ _ _ _ _} ()
subst-zeroᵘ {t = set _ _ _ _ _ _} ()
subst-zeroᵘ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-sucᵘ {t = Quot _ _} ()
wk-sucᵘ {t = class _} ()
wk-sucᵘ {t = resp _ _ _ _ _} ()
wk-sucᵘ {t = set _ _ _ _ _ _} ()
wk-sucᵘ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-sucᵘ {t = Quot _ _} ()
subst-sucᵘ {t = class _} ()
subst-sucᵘ {t = resp _ _ _ _ _} ()
subst-sucᵘ {t = set _ _ _ _ _ _} ()
subst-sucᵘ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-supᵘ {t = Quot _ _} ()
wk-supᵘ {t = class _} ()
wk-supᵘ {t = resp _ _ _ _ _} ()
wk-supᵘ {t = set _ _ _ _ _ _} ()
wk-supᵘ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-supᵘ {t = Quot _ _} ()
subst-supᵘ {t = class _} ()
subst-supᵘ {t = resp _ _ _ _ _} ()
subst-supᵘ {t = set _ _ _ _ _ _} ()
subst-supᵘ {t = qrec _ _ _ _ _} ()
wk-ωᵘ+ : wk ρ l ≡ ωᵘ+ m → l ≡ ωᵘ+ m
wk-ωᵘ+ {l = ωᵘ+ _} refl = refl
wk-ωᵘ+ {l = level _} ()
subst-ωᵘ+ : l [ σ ] ≡ ωᵘ+ m → l ≡ ωᵘ+ m
subst-ωᵘ+ {l = ωᵘ+ _} refl = refl
subst-ωᵘ+ {l = level _} ()
wk-level :
wk ρ l ≡ level t →
∃ λ t′ → l ≡ level t′ × wk ρ t′ ≡ t
wk-level {l = level _} refl = _ , refl , refl
wk-level {l = ωᵘ+ _} ()
subst-level :
l [ σ ] ≡ level t →
∃ λ t′ → l ≡ level t′ × t′ [ σ ] ≡ t
subst-level {l = level _} refl = _ , refl , refl
subst-level {l = ωᵘ+ _} ()
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 _ _ _ _ _ _} ()
wk-defn {t = Quot _ _} ()
wk-defn {t = class _} ()
wk-defn {t = resp _ _ _ _ _} ()
wk-defn {t = set _ _ _ _ _ _} ()
wk-defn {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-defn {t = Quot _ _} ()
subst-defn {t = class _} ()
subst-defn {t = resp _ _ _ _ _} ()
subst-defn {t = set _ _ _ _ _ _} ()
subst-defn {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-U {t = Quot _ _} ()
wk-U {t = class _} ()
wk-U {t = resp _ _ _ _ _} ()
wk-U {t = set _ _ _ _ _ _} ()
wk-U {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-U {t = Quot _ _} ()
subst-U {t = class _} ()
subst-U {t = resp _ _ _ _ _} ()
subst-U {t = set _ _ _ _ _ _} ()
subst-U {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-Lift {t = Quot _ _} ()
wk-Lift {t = class _} ()
wk-Lift {t = resp _ _ _ _ _} ()
wk-Lift {t = set _ _ _ _ _ _} ()
wk-Lift {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-Lift {t = Quot _ _} ()
subst-Lift {t = class _} ()
subst-Lift {t = resp _ _ _ _ _} ()
subst-Lift {t = set _ _ _ _ _ _} ()
subst-Lift {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-lift {t = Quot _ _} ()
wk-lift {t = class _} ()
wk-lift {t = resp _ _ _ _ _} ()
wk-lift {t = set _ _ _ _ _ _} ()
wk-lift {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-lift {t = Quot _ _} ()
subst-lift {t = class _} ()
subst-lift {t = resp _ _ _ _ _} ()
subst-lift {t = set _ _ _ _ _ _} ()
subst-lift {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-lower {t = Quot _ _} ()
wk-lower {t = class _} ()
wk-lower {t = resp _ _ _ _ _} ()
wk-lower {t = set _ _ _ _ _ _} ()
wk-lower {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-lower {t = Quot _ _} ()
subst-lower {t = class _} ()
subst-lower {t = resp _ _ _ _ _} ()
subst-lower {t = set _ _ _ _ _ _} ()
subst-lower {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-ΠΣ {t = Quot _ _} ()
wk-ΠΣ {t = class _} ()
wk-ΠΣ {t = resp _ _ _ _ _} ()
wk-ΠΣ {t = set _ _ _ _ _ _} ()
wk-ΠΣ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-ΠΣ {t = Quot _ _} ()
subst-ΠΣ {t = class _} ()
subst-ΠΣ {t = resp _ _ _ _ _} ()
subst-ΠΣ {t = set _ _ _ _ _ _} ()
subst-ΠΣ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-lam {t = Quot _ _} ()
wk-lam {t = class _} ()
wk-lam {t = resp _ _ _ _ _} ()
wk-lam {t = set _ _ _ _ _ _} ()
wk-lam {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-lam {t = Quot _ _} ()
subst-lam {t = class _} ()
subst-lam {t = resp _ _ _ _ _} ()
subst-lam {t = set _ _ _ _ _ _} ()
subst-lam {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-∘ {t = Quot _ _} ()
wk-∘ {t = class _} ()
wk-∘ {t = resp _ _ _ _ _} ()
wk-∘ {t = set _ _ _ _ _ _} ()
wk-∘ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-∘ {t = Quot _ _} ()
subst-∘ {t = class _} ()
subst-∘ {t = resp _ _ _ _ _} ()
subst-∘ {t = set _ _ _ _ _ _} ()
subst-∘ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-prod {t = Quot _ _} ()
wk-prod {t = class _} ()
wk-prod {t = resp _ _ _ _ _} ()
wk-prod {t = set _ _ _ _ _ _} ()
wk-prod {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-prod {t = Quot _ _} ()
subst-prod {t = class _} ()
subst-prod {t = resp _ _ _ _ _} ()
subst-prod {t = set _ _ _ _ _ _} ()
subst-prod {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-fst {t = Quot _ _} ()
wk-fst {t = class _} ()
wk-fst {t = resp _ _ _ _ _} ()
wk-fst {t = set _ _ _ _ _ _} ()
wk-fst {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-fst {t = Quot _ _} ()
subst-fst {t = class _} ()
subst-fst {t = resp _ _ _ _ _} ()
subst-fst {t = set _ _ _ _ _ _} ()
subst-fst {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-snd {t = Quot _ _} ()
wk-snd {t = class _} ()
wk-snd {t = resp _ _ _ _ _} ()
wk-snd {t = set _ _ _ _ _ _} ()
wk-snd {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-snd {t = Quot _ _} ()
subst-snd {t = class _} ()
subst-snd {t = resp _ _ _ _ _} ()
subst-snd {t = set _ _ _ _ _ _} ()
subst-snd {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-prodrec {t = Quot _ _} ()
wk-prodrec {t = class _} ()
wk-prodrec {t = resp _ _ _ _ _} ()
wk-prodrec {t = set _ _ _ _ _ _} ()
wk-prodrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-prodrec {t = Quot _ _} ()
subst-prodrec {t = class _} ()
subst-prodrec {t = resp _ _ _ _ _} ()
subst-prodrec {t = set _ _ _ _ _ _} ()
subst-prodrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-Unit {t = Quot _ _} ()
wk-Unit {t = class _} ()
wk-Unit {t = resp _ _ _ _ _} ()
wk-Unit {t = set _ _ _ _ _ _} ()
wk-Unit {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-Unit {t = Quot _ _} ()
subst-Unit {t = class _} ()
subst-Unit {t = resp _ _ _ _ _} ()
subst-Unit {t = set _ _ _ _ _ _} ()
subst-Unit {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-star {t = Quot _ _} ()
wk-star {t = class _} ()
wk-star {t = resp _ _ _ _ _} ()
wk-star {t = set _ _ _ _ _ _} ()
wk-star {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-star {t = Quot _ _} ()
subst-star {t = class _} ()
subst-star {t = resp _ _ _ _ _} ()
subst-star {t = set _ _ _ _ _ _} ()
subst-star {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-unitrec {t = Quot _ _} ()
wk-unitrec {t = class _} ()
wk-unitrec {t = resp _ _ _ _ _} ()
wk-unitrec {t = set _ _ _ _ _ _} ()
wk-unitrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-unitrec {t = Quot _ _} ()
subst-unitrec {t = class _} ()
subst-unitrec {t = resp _ _ _ _ _} ()
subst-unitrec {t = set _ _ _ _ _ _} ()
subst-unitrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-Empty {t = Quot _ _} ()
wk-Empty {t = class _} ()
wk-Empty {t = resp _ _ _ _ _} ()
wk-Empty {t = set _ _ _ _ _ _} ()
wk-Empty {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-Empty {t = Quot _ _} ()
subst-Empty {t = class _} ()
subst-Empty {t = resp _ _ _ _ _} ()
subst-Empty {t = set _ _ _ _ _ _} ()
subst-Empty {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-emptyrec {t = Quot _ _} ()
wk-emptyrec {t = class _} ()
wk-emptyrec {t = resp _ _ _ _ _} ()
wk-emptyrec {t = set _ _ _ _ _ _} ()
wk-emptyrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-emptyrec {t = Quot _ _} ()
subst-emptyrec {t = class _} ()
subst-emptyrec {t = resp _ _ _ _ _} ()
subst-emptyrec {t = set _ _ _ _ _ _} ()
subst-emptyrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-ℕ {t = Quot _ _} ()
wk-ℕ {t = class _} ()
wk-ℕ {t = resp _ _ _ _ _} ()
wk-ℕ {t = set _ _ _ _ _ _} ()
wk-ℕ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-ℕ {t = Quot _ _} ()
subst-ℕ {t = class _} ()
subst-ℕ {t = resp _ _ _ _ _} ()
subst-ℕ {t = set _ _ _ _ _ _} ()
subst-ℕ {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-zero {t = Quot _ _} ()
wk-zero {t = class _} ()
wk-zero {t = resp _ _ _ _ _} ()
wk-zero {t = set _ _ _ _ _ _} ()
wk-zero {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-zero {t = Quot _ _} ()
subst-zero {t = class _} ()
subst-zero {t = resp _ _ _ _ _} ()
subst-zero {t = set _ _ _ _ _ _} ()
subst-zero {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-suc {t = Quot _ _} ()
wk-suc {t = class _} ()
wk-suc {t = resp _ _ _ _ _} ()
wk-suc {t = set _ _ _ _ _ _} ()
wk-suc {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-suc {t = Quot _ _} ()
subst-suc {t = class _} ()
subst-suc {t = resp _ _ _ _ _} ()
subst-suc {t = set _ _ _ _ _ _} ()
subst-suc {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-natrec {t = Quot _ _} ()
wk-natrec {t = class _} ()
wk-natrec {t = resp _ _ _ _ _} ()
wk-natrec {t = set _ _ _ _ _ _} ()
wk-natrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-natrec {t = Quot _ _} ()
subst-natrec {t = class _} ()
subst-natrec {t = resp _ _ _ _ _} ()
subst-natrec {t = set _ _ _ _ _ _} ()
subst-natrec {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-Id {v = Quot _ _} ()
wk-Id {v = class _} ()
wk-Id {v = resp _ _ _ _ _} ()
wk-Id {v = set _ _ _ _ _ _} ()
wk-Id {v = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-Id {v = Quot _ _} ()
subst-Id {v = class _} ()
subst-Id {v = resp _ _ _ _ _} ()
subst-Id {v = set _ _ _ _ _ _} ()
subst-Id {v = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-rfl {t = Quot _ _} ()
wk-rfl {t = class _} ()
wk-rfl {t = resp _ _ _ _ _} ()
wk-rfl {t = set _ _ _ _ _ _} ()
wk-rfl {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-rfl {t = Quot _ _} ()
subst-rfl {t = class _} ()
subst-rfl {t = resp _ _ _ _ _} ()
subst-rfl {t = set _ _ _ _ _ _} ()
subst-rfl {t = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-J {w = Quot _ _} ()
wk-J {w = class _} ()
wk-J {w = resp _ _ _ _ _} ()
wk-J {w = set _ _ _ _ _ _} ()
wk-J {w = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-J {w = Quot _ _} ()
subst-J {w = class _} ()
subst-J {w = resp _ _ _ _ _} ()
subst-J {w = set _ _ _ _ _ _} ()
subst-J {w = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-K {w = Quot _ _} ()
wk-K {w = class _} ()
wk-K {w = resp _ _ _ _ _} ()
wk-K {w = set _ _ _ _ _ _} ()
wk-K {w = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-K {w = Quot _ _} ()
subst-K {w = class _} ()
subst-K {w = resp _ _ _ _ _} ()
subst-K {w = set _ _ _ _ _ _} ()
subst-K {w = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
wk-[]-cong {w = Quot _ _} ()
wk-[]-cong {w = class _} ()
wk-[]-cong {w = resp _ _ _ _ _} ()
wk-[]-cong {w = set _ _ _ _ _ _} ()
wk-[]-cong {w = qrec _ _ _ _ _} ()
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 _ _ _ _ _ _} ()
subst-[]-cong {w = Quot _ _} ()
subst-[]-cong {w = class _} ()
subst-[]-cong {w = resp _ _ _ _ _} ()
subst-[]-cong {w = set _ _ _ _ _ _} ()
subst-[]-cong {w = qrec _ _ _ _ _} ()
wk-Quot :
wk ρ t ≡ Quot A B →
∃₂ λ A′ B′ → t ≡ Quot A′ B′ × wk ρ A′ ≡ A × wk (liftn ρ 2) B′ ≡ B
wk-Quot {t = Quot _ _} refl =
_ , _ , refl , refl , refl
wk-Quot {t = var _} ()
wk-Quot {t = defn _} ()
wk-Quot {t = U _} ()
wk-Quot {t = Level} ()
wk-Quot {t = zeroᵘ} ()
wk-Quot {t = sucᵘ _} ()
wk-Quot {t = _ supᵘ _} ()
wk-Quot {t = Lift _ _} ()
wk-Quot {t = lift _} ()
wk-Quot {t = lower _} ()
wk-Quot {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-Quot {t = lam _ _} ()
wk-Quot {t = _ ∘⟨ _ ⟩ _} ()
wk-Quot {t = prod _ _ _ _} ()
wk-Quot {t = fst _ _} ()
wk-Quot {t = snd _ _} ()
wk-Quot {t = prodrec _ _ _ _ _ _} ()
wk-Quot {t = Empty} ()
wk-Quot {t = emptyrec _ _ _} ()
wk-Quot {t = Unit _} ()
wk-Quot {t = star _} ()
wk-Quot {t = unitrec _ _ _ _ _} ()
wk-Quot {t = ℕ} ()
wk-Quot {t = zero} ()
wk-Quot {t = suc _} ()
wk-Quot {t = natrec _ _ _ _ _ _ _} ()
wk-Quot {t = Id _ _ _} ()
wk-Quot {t = rfl} ()
wk-Quot {t = J _ _ _ _ _ _ _ _} ()
wk-Quot {t = K _ _ _ _ _ _} ()
wk-Quot {t = []-cong _ _ _ _ _ _} ()
wk-Quot {t = class _} ()
wk-Quot {t = resp _ _ _ _ _} ()
wk-Quot {t = set _ _ _ _ _ _} ()
wk-Quot {t = qrec _ _ _ _ _} ()
subst-Quot :
t [ σ ] ≡ Quot A B →
(∃ λ x → t ≡ var x) ⊎
∃₂ λ A′ B′ → t ≡ Quot A′ B′ × A′ [ σ ] ≡ A × B′ [ σ ⇑[ 2 ] ] ≡ B
subst-Quot {t = var _} _ =
inj₁ (_ , refl)
subst-Quot {t = Quot _ _} refl =
inj₂ (_ , _ , refl , refl , refl)
subst-Quot {t = defn _} ()
subst-Quot {t = U _} ()
subst-Quot {t = Level} ()
subst-Quot {t = zeroᵘ} ()
subst-Quot {t = sucᵘ _} ()
subst-Quot {t = _ supᵘ _} ()
subst-Quot {t = Lift _ _} ()
subst-Quot {t = lift _} ()
subst-Quot {t = lower _} ()
subst-Quot {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-Quot {t = lam _ _} ()
subst-Quot {t = _ ∘⟨ _ ⟩ _} ()
subst-Quot {t = prod _ _ _ _} ()
subst-Quot {t = fst _ _} ()
subst-Quot {t = snd _ _} ()
subst-Quot {t = prodrec _ _ _ _ _ _} ()
subst-Quot {t = Empty} ()
subst-Quot {t = emptyrec _ _ _} ()
subst-Quot {t = Unit _} ()
subst-Quot {t = star _} ()
subst-Quot {t = unitrec _ _ _ _ _} ()
subst-Quot {t = ℕ} ()
subst-Quot {t = zero} ()
subst-Quot {t = suc _} ()
subst-Quot {t = natrec _ _ _ _ _ _ _} ()
subst-Quot {t = Id _ _ _} ()
subst-Quot {t = rfl} ()
subst-Quot {t = J _ _ _ _ _ _ _ _} ()
subst-Quot {t = K _ _ _ _ _ _} ()
subst-Quot {t = []-cong _ _ _ _ _ _} ()
subst-Quot {t = class _} ()
subst-Quot {t = resp _ _ _ _ _} ()
subst-Quot {t = set _ _ _ _ _ _} ()
subst-Quot {t = qrec _ _ _ _ _} ()
wk-class :
wk ρ t ≡ class u →
∃ λ u′ → t ≡ class u′ × wk ρ u′ ≡ u
wk-class {t = class _} refl =
_ , refl , refl
wk-class {t = var _} ()
wk-class {t = defn _} ()
wk-class {t = U _} ()
wk-class {t = Level} ()
wk-class {t = zeroᵘ} ()
wk-class {t = sucᵘ _} ()
wk-class {t = _ supᵘ _} ()
wk-class {t = Lift _ _} ()
wk-class {t = lift _} ()
wk-class {t = lower _} ()
wk-class {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-class {t = lam _ _} ()
wk-class {t = _ ∘⟨ _ ⟩ _} ()
wk-class {t = prod _ _ _ _} ()
wk-class {t = fst _ _} ()
wk-class {t = snd _ _} ()
wk-class {t = prodrec _ _ _ _ _ _} ()
wk-class {t = Empty} ()
wk-class {t = emptyrec _ _ _} ()
wk-class {t = Unit _} ()
wk-class {t = star _} ()
wk-class {t = unitrec _ _ _ _ _} ()
wk-class {t = ℕ} ()
wk-class {t = zero} ()
wk-class {t = suc _} ()
wk-class {t = natrec _ _ _ _ _ _ _} ()
wk-class {t = Id _ _ _} ()
wk-class {t = rfl} ()
wk-class {t = J _ _ _ _ _ _ _ _} ()
wk-class {t = K _ _ _ _ _ _} ()
wk-class {t = []-cong _ _ _ _ _ _} ()
wk-class {t = Quot _ _} ()
wk-class {t = resp _ _ _ _ _} ()
wk-class {t = set _ _ _ _ _ _} ()
wk-class {t = qrec _ _ _ _ _} ()
subst-class :
t [ σ ] ≡ class u →
(∃ λ x → t ≡ var x) ⊎
∃ λ u′ → t ≡ class u′ × u′ [ σ ] ≡ u
subst-class {t = var _} _ =
inj₁ (_ , refl)
subst-class {t = class _} refl =
inj₂ (_ , refl , refl)
subst-class {t = defn _} ()
subst-class {t = U _} ()
subst-class {t = Level} ()
subst-class {t = zeroᵘ} ()
subst-class {t = sucᵘ _} ()
subst-class {t = _ supᵘ _} ()
subst-class {t = Lift _ _} ()
subst-class {t = lift _} ()
subst-class {t = lower _} ()
subst-class {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-class {t = lam _ _} ()
subst-class {t = _ ∘⟨ _ ⟩ _} ()
subst-class {t = prod _ _ _ _} ()
subst-class {t = fst _ _} ()
subst-class {t = snd _ _} ()
subst-class {t = prodrec _ _ _ _ _ _} ()
subst-class {t = Empty} ()
subst-class {t = emptyrec _ _ _} ()
subst-class {t = Unit _} ()
subst-class {t = star _} ()
subst-class {t = unitrec _ _ _ _ _} ()
subst-class {t = ℕ} ()
subst-class {t = zero} ()
subst-class {t = suc _} ()
subst-class {t = natrec _ _ _ _ _ _ _} ()
subst-class {t = Id _ _ _} ()
subst-class {t = rfl} ()
subst-class {t = J _ _ _ _ _ _ _ _} ()
subst-class {t = K _ _ _ _ _ _} ()
subst-class {t = []-cong _ _ _ _ _ _} ()
subst-class {t = Quot _ _} ()
subst-class {t = resp _ _ _ _ _} ()
subst-class {t = set _ _ _ _ _ _} ()
subst-class {t = qrec _ _ _ _ _} ()
wk-resp :
wk ρ t ≡ resp A B u v w →
∃₅ λ A′ B′ u′ v′ w′ →
t ≡ resp A′ B′ u′ v′ w′ × wk ρ A′ ≡ A × wk (liftn ρ 2) B′ ≡ B ×
wk ρ u′ ≡ u × wk ρ v′ ≡ v × wk ρ w′ ≡ w
wk-resp {t = resp _ _ _ _ _} refl =
_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl
wk-resp {t = var _} ()
wk-resp {t = defn _} ()
wk-resp {t = U _} ()
wk-resp {t = Level} ()
wk-resp {t = zeroᵘ} ()
wk-resp {t = sucᵘ _} ()
wk-resp {t = _ supᵘ _} ()
wk-resp {t = Lift _ _} ()
wk-resp {t = lift _} ()
wk-resp {t = lower _} ()
wk-resp {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-resp {t = lam _ _} ()
wk-resp {t = _ ∘⟨ _ ⟩ _} ()
wk-resp {t = prod _ _ _ _} ()
wk-resp {t = fst _ _} ()
wk-resp {t = snd _ _} ()
wk-resp {t = prodrec _ _ _ _ _ _} ()
wk-resp {t = Empty} ()
wk-resp {t = emptyrec _ _ _} ()
wk-resp {t = Unit _} ()
wk-resp {t = star _} ()
wk-resp {t = unitrec _ _ _ _ _} ()
wk-resp {t = ℕ} ()
wk-resp {t = zero} ()
wk-resp {t = suc _} ()
wk-resp {t = natrec _ _ _ _ _ _ _} ()
wk-resp {t = Id _ _ _} ()
wk-resp {t = rfl} ()
wk-resp {t = J _ _ _ _ _ _ _ _} ()
wk-resp {t = K _ _ _ _ _ _} ()
wk-resp {t = []-cong _ _ _ _ _ _} ()
wk-resp {t = Quot _ _} ()
wk-resp {t = class _} ()
wk-resp {t = set _ _ _ _ _ _} ()
wk-resp {t = qrec _ _ _ _ _} ()
subst-resp :
t [ σ ] ≡ resp A B u v w →
(∃ λ x → t ≡ var x) ⊎
∃₅ λ A′ B′ u′ v′ w′ →
t ≡ resp A′ B′ u′ v′ w′ × A′ [ σ ] ≡ A × B′ [ σ ⇑[ 2 ] ] ≡ B ×
u′ [ σ ] ≡ u × v′ [ σ ] ≡ v × w′ [ σ ] ≡ w
subst-resp {t = var _} _ =
inj₁ (_ , refl)
subst-resp {t = resp _ _ _ _ _} refl =
inj₂ (_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl)
subst-resp {t = defn _} ()
subst-resp {t = U _} ()
subst-resp {t = Level} ()
subst-resp {t = zeroᵘ} ()
subst-resp {t = sucᵘ _} ()
subst-resp {t = _ supᵘ _} ()
subst-resp {t = Lift _ _} ()
subst-resp {t = lift _} ()
subst-resp {t = lower _} ()
subst-resp {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-resp {t = lam _ _} ()
subst-resp {t = _ ∘⟨ _ ⟩ _} ()
subst-resp {t = prod _ _ _ _} ()
subst-resp {t = fst _ _} ()
subst-resp {t = snd _ _} ()
subst-resp {t = prodrec _ _ _ _ _ _} ()
subst-resp {t = Empty} ()
subst-resp {t = emptyrec _ _ _} ()
subst-resp {t = Unit _} ()
subst-resp {t = star _} ()
subst-resp {t = unitrec _ _ _ _ _} ()
subst-resp {t = ℕ} ()
subst-resp {t = zero} ()
subst-resp {t = suc _} ()
subst-resp {t = natrec _ _ _ _ _ _ _} ()
subst-resp {t = Id _ _ _} ()
subst-resp {t = rfl} ()
subst-resp {t = J _ _ _ _ _ _ _ _} ()
subst-resp {t = K _ _ _ _ _ _} ()
subst-resp {t = []-cong _ _ _ _ _ _} ()
subst-resp {t = Quot _ _} ()
subst-resp {t = class _} ()
subst-resp {t = set _ _ _ _ _ _} ()
subst-resp {t = qrec _ _ _ _ _} ()
wk-set :
wk ρ t ≡ set A₁ A₂ u₁ u₂ u₃ u₄ →
∃₆ λ A₁′ A₂′ u₁′ u₂′ u₃′ u₄′ →
t ≡ set A₁′ A₂′ u₁′ u₂′ u₃′ u₄′ × wk ρ A₁′ ≡ A₁ ×
wk (liftn ρ 2) A₂′ ≡ A₂ × wk ρ u₁′ ≡ u₁ × wk ρ u₂′ ≡ u₂ ×
wk ρ u₃′ ≡ u₃ × wk ρ u₄′ ≡ u₄
wk-set {t = set _ _ _ _ _ _} refl =
_ , _ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl , refl
wk-set {t = var _} ()
wk-set {t = defn _} ()
wk-set {t = U _} ()
wk-set {t = Level} ()
wk-set {t = zeroᵘ} ()
wk-set {t = sucᵘ _} ()
wk-set {t = _ supᵘ _} ()
wk-set {t = Lift _ _} ()
wk-set {t = lift _} ()
wk-set {t = lower _} ()
wk-set {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-set {t = lam _ _} ()
wk-set {t = _ ∘⟨ _ ⟩ _} ()
wk-set {t = prod _ _ _ _} ()
wk-set {t = fst _ _} ()
wk-set {t = snd _ _} ()
wk-set {t = prodrec _ _ _ _ _ _} ()
wk-set {t = Empty} ()
wk-set {t = emptyrec _ _ _} ()
wk-set {t = Unit _} ()
wk-set {t = star _} ()
wk-set {t = unitrec _ _ _ _ _} ()
wk-set {t = ℕ} ()
wk-set {t = zero} ()
wk-set {t = suc _} ()
wk-set {t = natrec _ _ _ _ _ _ _} ()
wk-set {t = Id _ _ _} ()
wk-set {t = rfl} ()
wk-set {t = J _ _ _ _ _ _ _ _} ()
wk-set {t = K _ _ _ _ _ _} ()
wk-set {t = []-cong _ _ _ _ _ _} ()
wk-set {t = Quot _ _} ()
wk-set {t = class _} ()
wk-set {t = resp _ _ _ _ _} ()
wk-set {t = qrec _ _ _ _ _} ()
subst-set :
t [ σ ] ≡ set A₁ A₂ u₁ u₂ u₃ u₄ →
(∃ λ x → t ≡ var x) ⊎
∃₆ λ A₁′ A₂′ u₁′ u₂′ u₃′ u₄′ →
t ≡ set A₁′ A₂′ u₁′ u₂′ u₃′ u₄′ × A₁′ [ σ ] ≡ A₁ ×
A₂′ [ σ ⇑[ 2 ] ] ≡ A₂ × u₁′ [ σ ] ≡ u₁ × u₂′ [ σ ] ≡ u₂ ×
u₃′ [ σ ] ≡ u₃ × u₄′ [ σ ] ≡ u₄
subst-set {t = var _} _ =
inj₁ (_ , refl)
subst-set {t = set _ _ _ _ _ _} refl =
inj₂
(_ , _ , _ , _ , _ , _ ,
refl , refl , refl , refl , refl , refl , refl)
subst-set {t = defn _} ()
subst-set {t = U _} ()
subst-set {t = Level} ()
subst-set {t = zeroᵘ} ()
subst-set {t = sucᵘ _} ()
subst-set {t = _ supᵘ _} ()
subst-set {t = Lift _ _} ()
subst-set {t = lift _} ()
subst-set {t = lower _} ()
subst-set {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-set {t = lam _ _} ()
subst-set {t = _ ∘⟨ _ ⟩ _} ()
subst-set {t = prod _ _ _ _} ()
subst-set {t = fst _ _} ()
subst-set {t = snd _ _} ()
subst-set {t = prodrec _ _ _ _ _ _} ()
subst-set {t = Empty} ()
subst-set {t = emptyrec _ _ _} ()
subst-set {t = Unit _} ()
subst-set {t = star _} ()
subst-set {t = unitrec _ _ _ _ _} ()
subst-set {t = ℕ} ()
subst-set {t = zero} ()
subst-set {t = suc _} ()
subst-set {t = natrec _ _ _ _ _ _ _} ()
subst-set {t = Id _ _ _} ()
subst-set {t = rfl} ()
subst-set {t = J _ _ _ _ _ _ _ _} ()
subst-set {t = K _ _ _ _ _ _} ()
subst-set {t = []-cong _ _ _ _ _ _} ()
subst-set {t = Quot _ _} ()
subst-set {t = class _} ()
subst-set {t = resp _ _ _ _ _} ()
subst-set {t = qrec _ _ _ _ _} ()
wk-qrec :
wk ρ t ≡ qrec A u₁ u₂ u₃ u₄ →
∃₅ λ A′ u₁′ u₂′ u₃′ u₄′ →
t ≡ qrec A′ u₁′ u₂′ u₃′ u₄′ ×
wk (lift ρ) A′ ≡ A × wk (lift ρ) u₁′ ≡ u₁ ×
wk (liftn ρ 3) u₂′ ≡ u₂ × wk (liftn ρ 5) u₃′ ≡ u₃ × wk ρ u₄′ ≡ u₄
wk-qrec {t = qrec _ _ _ _ _} refl =
_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl
wk-qrec {t = var _} ()
wk-qrec {t = defn _} ()
wk-qrec {t = U _} ()
wk-qrec {t = Level} ()
wk-qrec {t = zeroᵘ} ()
wk-qrec {t = sucᵘ _} ()
wk-qrec {t = _ supᵘ _} ()
wk-qrec {t = Lift _ _} ()
wk-qrec {t = lift _} ()
wk-qrec {t = lower _} ()
wk-qrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
wk-qrec {t = lam _ _} ()
wk-qrec {t = _ ∘⟨ _ ⟩ _} ()
wk-qrec {t = prod _ _ _ _} ()
wk-qrec {t = fst _ _} ()
wk-qrec {t = snd _ _} ()
wk-qrec {t = prodrec _ _ _ _ _ _} ()
wk-qrec {t = Empty} ()
wk-qrec {t = emptyrec _ _ _} ()
wk-qrec {t = Unit _} ()
wk-qrec {t = star _} ()
wk-qrec {t = unitrec _ _ _ _ _} ()
wk-qrec {t = ℕ} ()
wk-qrec {t = zero} ()
wk-qrec {t = suc _} ()
wk-qrec {t = natrec _ _ _ _ _ _ _} ()
wk-qrec {t = Id _ _ _} ()
wk-qrec {t = rfl} ()
wk-qrec {t = J _ _ _ _ _ _ _ _} ()
wk-qrec {t = K _ _ _ _ _ _} ()
wk-qrec {t = []-cong _ _ _ _ _ _} ()
wk-qrec {t = Quot _ _} ()
wk-qrec {t = class _} ()
wk-qrec {t = resp _ _ _ _ _} ()
wk-qrec {t = set _ _ _ _ _ _} ()
subst-qrec :
t [ σ ] ≡ qrec A u₁ u₂ u₃ u₄ →
(∃ λ x → t ≡ var x) ⊎
∃₅ λ A′ u₁′ u₂′ u₃′ u₄′ →
t ≡ qrec A′ u₁′ u₂′ u₃′ u₄′ ×
A′ [ σ ⇑ ] ≡ A × u₁′ [ σ ⇑ ] ≡ u₁ × u₂′ [ σ ⇑[ 3 ] ] ≡ u₂ ×
u₃′ [ σ ⇑[ 5 ] ] ≡ u₃ × u₄′ [ σ ] ≡ u₄
subst-qrec {t = var _} _ =
inj₁ (_ , refl)
subst-qrec {t = qrec _ _ _ _ _} refl =
inj₂ (_ , _ , _ , _ , _ , refl , refl , refl , refl , refl , refl)
subst-qrec {t = defn _} ()
subst-qrec {t = U _} ()
subst-qrec {t = Level} ()
subst-qrec {t = zeroᵘ} ()
subst-qrec {t = sucᵘ _} ()
subst-qrec {t = _ supᵘ _} ()
subst-qrec {t = Lift _ _} ()
subst-qrec {t = lift _} ()
subst-qrec {t = lower _} ()
subst-qrec {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} ()
subst-qrec {t = lam _ _} ()
subst-qrec {t = _ ∘⟨ _ ⟩ _} ()
subst-qrec {t = prod _ _ _ _} ()
subst-qrec {t = fst _ _} ()
subst-qrec {t = snd _ _} ()
subst-qrec {t = prodrec _ _ _ _ _ _} ()
subst-qrec {t = Empty} ()
subst-qrec {t = emptyrec _ _ _} ()
subst-qrec {t = Unit _} ()
subst-qrec {t = star _} ()
subst-qrec {t = unitrec _ _ _ _ _} ()
subst-qrec {t = ℕ} ()
subst-qrec {t = zero} ()
subst-qrec {t = suc _} ()
subst-qrec {t = natrec _ _ _ _ _ _ _} ()
subst-qrec {t = Id _ _ _} ()
subst-qrec {t = rfl} ()
subst-qrec {t = J _ _ _ _ _ _ _ _} ()
subst-qrec {t = K _ _ _ _ _ _} ()
subst-qrec {t = []-cong _ _ _ _ _ _} ()
subst-qrec {t = Quot _ _} ()
subst-qrec {t = class _} ()
subst-qrec {t = resp _ _ _ _ _} ()
subst-qrec {t = set _ _ _ _ _ _} ()