open import Data.Universe.Indexed
module deBruijn.Substitution.Data.Application.Application21
{i u e} {Uni : IndexedUniverse i u e} where
import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Application.Application
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Map
open import deBruijn.Substitution.Data.Simple
open import Function using (_$_)
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P
open P.≡-Reasoning
record Application₂₁
{t₁} {T₁ : Term-like t₁}
{t₂} {T₂ : Term-like t₂}
(simple₁ : Simple T₁)
(simple₂ : Simple T₂)
(trans : [ T₁ ⟶⁼ T₂ ])
: Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
open Term-like T₁ using () renaming (_⊢_ to _⊢₁_; _≅-⊢_ to _≅-⊢₁_)
open Term-like T₂ using ([_]) renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_)
open Simple simple₁
using ()
renaming ( id to id₁; sub to sub₁; var to var₁
; weaken[_] to weaken₁[_]; wk to wk₁
; wk-subst to wk-subst₁; wk-subst[_] to wk-subst₁[_]
; _↑ to _↑₁; _↑_ to _↑₁_; _↑⁺_ to _↑⁺₁_; _↑₊_ to _↑₊₁_
; _↑⋆_ to _↑⋆₁_; _↑⁺⋆_ to _↑⁺⋆₁_; _↑₊⋆_ to _↑₊⋆₁_
)
open Simple simple₂
using ()
renaming ( id to id₂; id[_] to id₂[_]; var to var₂
; weaken to weaken₂; weaken[_] to weaken₂[_]; wk to wk₂
; wk-subst to wk-subst₂; wk-subst[_] to wk-subst₂[_]
; _↑ to _↑₂; _↑_ to _↑₂_
)
field
application : Application T₁ T₂
open Application application
field
trans-weaken : ∀ {Γ σ τ} (t : Γ ⊢₁ τ) →
trans · (weaken₁[ σ ] · t) ≅-⊢₂
weaken₂[ σ ] · (trans · t)
trans-var : ∀ {Γ σ} (x : Γ ∋ σ) → trans · (var₁ · x) ≅-⊢₂ var₂ · x
var-/⊢ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρ : Sub T₁ ρ̂) →
var₂ · x /⊢ ρ ≅-⊢₂ trans · (x /∋ ρ)
app∋⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T₁ ρ̂ → [ Var ⟶ T₂ ] ρ̂
app∋⋆ ε = var₂
app∋⋆ (ε ▻ ρ) = trans [∘] app∋ ρ
app∋⋆ (ρs ▻ ρ) = app ρ [∘] app∋⋆ ρs
infixl 8 _/∋⋆_
_/∋⋆_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ∋ σ → Subs T₁ ρ̂ → Δ ⊢₂ σ /̂ ρ̂
x /∋⋆ ρs = app∋⋆ ρs · x
∘⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T₁ ρ̂ → Sub T₂ ρ̂
∘⋆ ε = id₂
∘⋆ (ρs ▻ ρ) = ∘⋆ ρs ∘ ρ
trans-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢₁ σ₁}
{Γ₂ σ₂} {t₂ : Γ₂ ⊢₁ σ₂} →
t₁ ≅-⊢₁ t₂ → trans · t₁ ≅-⊢₂ trans · t₂
trans-cong P.refl = P.refl
app∋⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
ρs₁ ≅-⇨⋆ ρs₂ → app∋⋆ ρs₁ ≅-⟶ app∋⋆ ρs₂
app∋⋆-cong P.refl = [ P.refl ]
/∋⋆-cong :
∀ {Γ₁ Δ₁ σ₁} {x₁ : Γ₁ ∋ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
{Γ₂ Δ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
x₁ ≅-∋ x₂ → ρs₁ ≅-⇨⋆ ρs₂ → x₁ /∋⋆ ρs₁ ≅-⊢₂ x₂ /∋⋆ ρs₂
/∋⋆-cong P.refl P.refl = P.refl
∘⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
ρs₁ ≅-⇨⋆ ρs₂ → ∘⋆ ρs₁ ≅-⇨ ∘⋆ ρs₂
∘⋆-cong P.refl = P.refl
abstract
/∋-∘⋆ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρs : Subs T₁ ρ̂) →
x /∋ ∘⋆ ρs ≅-⊢₂ var₂ · x /⊢⋆ ρs
/∋-∘⋆ x ε = begin
[ x /∋ id₂ ] ≡⟨ Simple./∋-id simple₂ x ⟩
[ var₂ · x ] ∎
/∋-∘⋆ x (ρs ▻ ρ) = begin
[ x /∋ ∘⋆ ρs ∘ ρ ] ≡⟨ /∋-∘ x (∘⋆ ρs) ρ ⟩
[ x /∋ ∘⋆ ρs /⊢ ρ ] ≡⟨ /⊢-cong (/∋-∘⋆ x ρs) P.refl ⟩
[ var₂ · x /⊢⋆ ρs /⊢ ρ ] ∎
var-/⊢⋆ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρs : Subs T₁ ρ̂) →
var₂ · x /⊢⋆ ρs ≅-⊢₂ x /∋⋆ ρs
var-/⊢⋆ x ε = P.refl
var-/⊢⋆ x (ε ▻ ρ) = begin
[ var₂ · x /⊢ ρ ] ≡⟨ var-/⊢ x ρ ⟩
[ trans · (x /∋ ρ) ] ∎
var-/⊢⋆ x (ρs ▻ ρ₁ ▻ ρ₂) = begin
[ var₂ · x /⊢⋆ (ρs ▻ ρ₁) /⊢ ρ₂ ] ≡⟨ /⊢-cong (var-/⊢⋆ x (ρs ▻ ρ₁)) P.refl ⟩
[ x /∋⋆ (ρs ▻ ρ₁) /⊢ ρ₂ ] ∎
/∋-≅-⊢-var : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}
(x : Γ ∋ σ) (ρ : Sub T₁ ρ̂) {y : Δ ∋ σ / ρ} →
x /∋ ρ ≅-⊢₁ var₁ · y →
var₂ · x /⊢ ρ ≅-⊢₂ var₂ · y
/∋-≅-⊢-var x ρ {y} hyp = begin
[ var₂ · x /⊢ ρ ] ≡⟨ var-/⊢ x ρ ⟩
[ trans · (x /∋ ρ) ] ≡⟨ trans-cong hyp ⟩
[ trans · (var₁ · y) ] ≡⟨ trans-var y ⟩
[ var₂ · y ] ∎
var-/⊢-id : ∀ {Γ σ} (x : Γ ∋ σ) → var₂ · x /⊢ id₁ ≅-⊢₂ var₂ · x
var-/⊢-id x = /∋-≅-⊢-var x id₁ (Simple./∋-id simple₁ x)
var-/⊢-wk-↑⁺ : ∀ {Γ σ} Γ⁺ {τ} (x : Γ ++⁺ Γ⁺ ∋ τ) →
var₂ · x /⊢ wk₁ {σ = σ} ↑⁺₁ Γ⁺ ≅-⊢₂
var₂ · (lift weaken∋[ σ ] Γ⁺ · x)
var-/⊢-wk-↑⁺ Γ⁺ x =
/∋-≅-⊢-var x (wk₁ ↑⁺₁ Γ⁺) (Simple./∋-wk-↑⁺ simple₁ Γ⁺ x)
var-/⊢-wk-↑⁺-↑⁺ : ∀ {Γ σ} Γ⁺ Γ⁺⁺ {τ} (x : Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ∋ τ) →
var₂ · x /⊢ wk₁ {σ = σ} ↑⁺₁ Γ⁺ ↑⁺₁ Γ⁺⁺ ≅-⊢₂
var₂ · (lift (lift weaken∋[ σ ] Γ⁺) Γ⁺⁺ · x)
var-/⊢-wk-↑⁺-↑⁺ Γ⁺ Γ⁺⁺ x =
/∋-≅-⊢-var x (wk₁ ↑⁺₁ Γ⁺ ↑⁺₁ Γ⁺⁺)
(Simple./∋-wk-↑⁺-↑⁺ simple₁ Γ⁺ Γ⁺⁺ x)
zero-/⊢-↑ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} σ (ρ : Sub T₁ ρ̂) →
var₂ · zero /⊢ ρ ↑₁ σ ≅-⊢₂ var₂ · zero[ σ / ρ ]
zero-/⊢-↑ σ ρ =
/∋-≅-⊢-var zero (ρ ↑₁ σ) (Simple.zero-/∋-↑ simple₁ σ ρ)
zero-/⊢⋆-↑⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} σ (ρs : Subs T₁ ρ̂) →
var₂ · zero /⊢⋆ ρs ↑⋆₁ σ ≅-⊢₂
var₂ · zero[ σ /⋆ ρs ]
zero-/⊢⋆-↑⋆ σ ε = P.refl
zero-/⊢⋆-↑⋆ σ (ρs ▻ ρ) = begin
[ var₂ · zero /⊢⋆ ρs ↑⋆₁ σ /⊢ ρ ↑₁ ] ≡⟨ /⊢-cong (zero-/⊢⋆-↑⋆ σ ρs) (P.refl {x = [ ρ ↑₁ (σ /⋆ ρs) ]}) ⟩
[ var₂ · zero /⊢ ρ ↑₁ (σ /⋆ ρs) ] ≡⟨ zero-/⊢-↑ (σ /⋆ ρs) ρ ⟩
[ var₂ · zero ] ∎
/⊢⋆-ε-↑⁺⋆ : ∀ {Γ} Γ⁺ {σ} (t : Γ ++⁺ Γ⁺ ⊢₂ σ) →
t /⊢⋆ ε ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t
/⊢⋆-ε-↑⁺⋆ Γ⁺ t = begin
[ t /⊢⋆ ε ↑⁺⋆₁ Γ⁺ ] ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.ε-↑⁺⋆ simple₁ Γ⁺) ⟩
[ t /⊢⋆ ε ] ≡⟨ P.refl ⟩
[ t ] ∎
/⊢⋆-ε-↑₊⋆ : ∀ {Γ} Γ₊ {σ} (t : Γ ++₊ Γ₊ ⊢₂ σ) →
t /⊢⋆ ε ↑₊⋆₁ Γ₊ ≅-⊢₂ t
/⊢⋆-ε-↑₊⋆ Γ₊ t = begin
[ t /⊢⋆ ε ↑₊⋆₁ Γ₊ ] ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.ε-↑₊⋆ simple₁ Γ₊) ⟩
[ t /⊢⋆ ε ] ≡⟨ P.refl ⟩
[ t ] ∎
/⊢⋆-▻-↑⁺⋆ :
∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ⁺ {σ}
(t : Γ ++⁺ Γ⁺ ⊢₂ σ) (ρs : Subs T₁ ρ̂₁) (ρ : Sub T₁ ρ̂₂) →
t /⊢⋆ (ρs ▻ ρ) ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t /⊢⋆ ρs ↑⁺⋆₁ Γ⁺ /⊢ ρ ↑⁺₁ (Γ⁺ /⁺⋆ ρs)
/⊢⋆-▻-↑⁺⋆ Γ⁺ t ρs ρ =
/⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑⁺⋆ simple₁ ρs ρ Γ⁺)
/⊢⋆-▻-↑₊⋆ :
∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ₊ {σ}
(t : Γ ++₊ Γ₊ ⊢₂ σ) (ρs : Subs T₁ ρ̂₁) (ρ : Sub T₁ ρ̂₂) →
t /⊢⋆ (ρs ▻ ρ) ↑₊⋆₁ Γ₊ ≅-⊢₂ t /⊢⋆ ρs ↑₊⋆₁ Γ₊ /⊢ ρ ↑₊₁ (Γ₊ /₊⋆ ρs)
/⊢⋆-▻-↑₊⋆ Γ₊ t ρs ρ =
/⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑₊⋆ simple₁ ρs ρ Γ₊)
/⊢⋆-ε-▻-↑⁺⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} Γ⁺ {σ}
(t : Γ ++⁺ Γ⁺ ⊢₂ σ) (ρ : Sub T₁ ρ̂) →
t /⊢⋆ (ε ▻ ρ) ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t /⊢ ρ ↑⁺₁ Γ⁺
/⊢⋆-ε-▻-↑⁺⋆ Γ⁺ t ρ = begin
[ t /⊢⋆ (ε ▻ ρ) ↑⁺⋆₁ Γ⁺ ] ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑⁺⋆ simple₁ ε ρ Γ⁺) ⟩
[ t /⊢⋆ ε ↑⁺⋆₁ Γ⁺ /⊢ ρ ↑⁺₁ (Γ⁺ /̂⁺ îd) ] ≡⟨ /⊢-cong (/⊢⋆-ε-↑⁺⋆ Γ⁺ t) (Simple.↑⁺-cong simple₁ P.refl (/̂⁺-îd Γ⁺)) ⟩
[ t /⊢ ρ ↑⁺₁ Γ⁺ ] ∎
/⊢⋆-ε-▻-▻-↑⁺⋆ :
∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ⁺ {σ}
(t : Γ ++⁺ Γ⁺ ⊢₂ σ) (ρ₁ : Sub T₁ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) →
t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑⁺⋆₁ Γ⁺ ≅-⊢₂
t /⊢ ρ₁ ↑⁺₁ Γ⁺ /⊢ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁)
/⊢⋆-ε-▻-▻-↑⁺⋆ Γ⁺ t ρ₁ ρ₂ = begin
[ t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑⁺⋆₁ Γ⁺ ] ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑⁺⋆ simple₁ (ε ▻ ρ₁) ρ₂ Γ⁺) ⟩
[ t /⊢⋆ (ε ▻ ρ₁) ↑⁺⋆₁ Γ⁺ /⊢ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁) ] ≡⟨ /⊢-cong (/⊢⋆-ε-▻-↑⁺⋆ Γ⁺ t ρ₁) P.refl ⟩
[ t /⊢ ρ₁ ↑⁺₁ Γ⁺ /⊢ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁) ] ∎
/⊢⋆-ε-▻-↑₊⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} Γ₊ {σ}
(t : Γ ++₊ Γ₊ ⊢₂ σ) (ρ : Sub T₁ ρ̂) →
t /⊢⋆ (ε ▻ ρ) ↑₊⋆₁ Γ₊ ≅-⊢₂ t /⊢ ρ ↑₊₁ Γ₊
/⊢⋆-ε-▻-↑₊⋆ Γ₊ t ρ = begin
[ t /⊢⋆ (ε ▻ ρ) ↑₊⋆₁ Γ₊ ] ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑₊⋆ simple₁ ε ρ Γ₊) ⟩
[ t /⊢⋆ ε ↑₊⋆₁ Γ₊ /⊢ ρ ↑₊₁ (Γ₊ /̂₊ îd) ] ≡⟨ /⊢-cong (/⊢⋆-ε-↑₊⋆ Γ₊ t) (Simple.↑₊-cong simple₁ P.refl (/̂₊-îd Γ₊)) ⟩
[ t /⊢ ρ ↑₊₁ Γ₊ ] ∎
/⊢⋆-ε-▻-▻-↑₊⋆ :
∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ₊ {σ}
(t : Γ ++₊ Γ₊ ⊢₂ σ) (ρ₁ : Sub T₁ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) →
t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑₊⋆₁ Γ₊ ≅-⊢₂
t /⊢ ρ₁ ↑₊₁ Γ₊ /⊢ ρ₂ ↑₊₁ (Γ₊ /₊ ρ₁)
/⊢⋆-ε-▻-▻-↑₊⋆ Γ₊ t ρ₁ ρ₂ = begin
[ t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑₊⋆₁ Γ₊ ] ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑₊⋆ simple₁ (ε ▻ ρ₁) ρ₂ Γ₊) ⟩
[ t /⊢⋆ (ε ▻ ρ₁) ↑₊⋆₁ Γ₊ /⊢ ρ₂ ↑₊₁ (Γ₊ /₊ ρ₁) ] ≡⟨ /⊢-cong (/⊢⋆-ε-▻-↑₊⋆ Γ₊ t ρ₁) P.refl ⟩
[ t /⊢ ρ₁ ↑₊₁ Γ₊ /⊢ ρ₂ ↑₊₁ (Γ₊ /₊ ρ₁) ] ∎
suc-/⊢-sub : ∀ {Γ σ τ} (x : Γ ∋ σ) (t : Γ ⊢₁ τ) →
var₂ · suc x /⊢ sub₁ t ≅-⊢₂ var₂ · x
suc-/⊢-sub x t = begin
[ var₂ · suc x /⊢ sub₁ t ] ≡⟨ var-/⊢ (suc x) (sub₁ t) ⟩
[ trans · (suc x /∋ sub₁ t) ] ≡⟨ P.refl ⟩
[ trans · (x /∋ id₁) ] ≡⟨ trans-cong (Simple./∋-id simple₁ x) ⟩
[ trans · (var₁ · x) ] ≡⟨ trans-var x ⟩
[ var₂ · x ] ∎
wk-∘-sub : ∀ {Γ σ} (t : Γ ⊢₁ σ) → wk₂ ∘ sub₁ t ≅-⇨ id₂[ Γ ]
wk-∘-sub t = extensionality P.refl λ x → begin
[ x /∋ wk₂ ∘ sub₁ t ] ≡⟨ /∋-∘ x wk₂ (sub₁ t) ⟩
[ x /∋ wk₂ /⊢ sub₁ t ] ≡⟨ /⊢-cong (Simple./∋-wk simple₂ x) P.refl ⟩
[ var₂ · suc x /⊢ sub₁ t ] ≡⟨ suc-/⊢-sub x t ⟩
[ var₂ · x ] ≡⟨ P.sym $ Simple./∋-id simple₂ x ⟩
[ x /∋ id₂ ] ∎
id-∘ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) → id₂ ∘ ρ ≅-⇨ map trans ρ
id-∘ ρ = extensionality P.refl λ x → begin
[ x /∋ id₂ ∘ ρ ] ≡⟨ /∋-∘ x id₂ ρ ⟩
[ x /∋ id₂ /⊢ ρ ] ≡⟨ /⊢-cong (Simple./∋-id simple₂ x) (P.refl {x = [ ρ ]}) ⟩
[ var₂ · x /⊢ ρ ] ≡⟨ var-/⊢ x ρ ⟩
[ trans · (x /∋ ρ) ] ≡⟨ P.sym $ /∋-map x trans ρ ⟩
[ x /∋ map trans ρ ] ∎
map-trans-wk-subst : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) →
map trans (wk-subst₁[ σ ] ρ) ≅-⇨
wk-subst₂[ σ ] (map trans ρ)
map-trans-wk-subst {σ = σ} ρ = begin
[ map trans (wk-subst₁[ σ ] ρ) ] ≡⟨ P.sym $ map-[∘] trans weaken₁[ σ ] ρ ⟩
[ map (trans [∘] weaken₁[ σ ]) ρ ] ≡⟨ map-cong-ext₁ P.refl trans-weaken (P.refl {x = [ ρ ]}) ⟩
[ map (weaken₂ [∘] trans) ρ ] ≡⟨ map-[∘] weaken₂ trans ρ ⟩
[ wk-subst₂ (map trans ρ) ] ∎
map-trans-↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) →
map trans (ρ ↑₁ σ) ≅-⇨ map trans ρ ↑₂ σ
map-trans-↑ {σ = σ} ρ = begin
[ map trans (ρ ↑₁ σ) ] ≡⟨ map-cong (trans ∎-⟶) (Simple.unfold-↑ simple₁ ρ) ⟩
[ map trans (wk-subst₁[ σ / ρ ] ρ ▻ var₁ · zero) ] ≡⟨ map-▻ trans (wk-subst₁ ρ) _ ⟩
[ map trans (wk-subst₁[ σ / ρ ] ρ) ▻ trans · (var₁ · zero) ] ≡⟨ ▻⇨-cong P.refl (map-trans-wk-subst ρ) (trans-var zero) ⟩
[ wk-subst₂ (map trans ρ) ▻ var₂ · zero ] ≡⟨ P.sym $ Simple.unfold-↑ simple₂ (map trans ρ) ⟩
[ map trans ρ ↑₂ ] ∎
open Application application public