From 62219722c00be55dd7773c65b0aa0b07e4dfdb02 Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 20 Apr 2018 14:45:00 -0300 Subject: [PATCH] syntax changes to Typed --- src/Typed.lagda | 274 ++++++++++++++++++++++++------------------------ 1 file changed, 138 insertions(+), 136 deletions(-) diff --git a/src/Typed.lagda b/src/Typed.lagda index fc16d88f..97db4a92 100644 --- a/src/Typed.lagda +++ b/src/Typed.lagda @@ -4,6 +4,7 @@ layout : page permalink : /Typed --- + ## Imports \begin{code} @@ -35,59 +36,60 @@ open import Collections using (_↔_) ## Syntax \begin{code} -infixr 6 _⇒_ +infixr 5 _⟹_ infixl 5 _,_⦂_ infix 4 _∋_⦂_ infix 4 _⊢_⦂_ -infix 5 ƛ_⦂_⇒_ -infix 5 ƛ_ +infix 5 `λ_⇒_ +infix 5 `λ_ infixl 6 _·_ +infix 7 `_ Id : Set Id = ℕ data Type : Set where - o : Type - _⇒_ : Type → Type → Type + `ℕ : Type + _⟹_ : Type → Type → Type data Env : Set where ε : Env _,_⦂_ : Env → Id → Type → Env data Term : Set where - ⌊_⌋ : Id → Term - ƛ_⦂_⇒_ : Id → Type → Term → Term - _·_ : Term → Term → Term + `_ : Id → Term + `λ_⇒_ : Id → Term → Term + _·_ : Term → Term → Term data _∋_⦂_ : Env → Id → Type → Set where - Z : ∀ {Γ A x} → - ----------------- - Γ , x ⦂ A ∋ x ⦂ A + Z : ∀ {Γ A x} + ----------------- + → Γ , x ⦂ A ∋ x ⦂ A - S : ∀ {Γ A B x y} → - x ≢ y → - Γ ∋ y ⦂ B → - ----------------- - Γ , x ⦂ A ∋ y ⦂ B + S : ∀ {Γ A B x y} + → x ≢ y + → Γ ∋ y ⦂ B + ----------------- + → Γ , x ⦂ A ∋ y ⦂ B data _⊢_⦂_ : Env → Term → Type → Set where - ⌊_⌋ : ∀ {Γ A x} → - Γ ∋ x ⦂ A → - --------------------- - Γ ⊢ ⌊ x ⌋ ⦂ A + `_ : ∀ {Γ A x} + → Γ ∋ x ⦂ A + --------------------- + → Γ ⊢ ` x ⦂ A - ƛ_ : ∀ {Γ x A N B} → - Γ , x ⦂ A ⊢ N ⦂ B → - -------------------------- - Γ ⊢ (ƛ x ⦂ A ⇒ N) ⦂ A ⇒ B + `λ_ : ∀ {Γ x A N B} + → Γ , x ⦂ A ⊢ N ⦂ B + ------------------------ + → Γ ⊢ (`λ x ⇒ N) ⦂ A ⟹ B - _·_ : ∀ {Γ L M A B} → - Γ ⊢ L ⦂ A ⇒ B → - Γ ⊢ M ⦂ A → - -------------- - Γ ⊢ L · M ⦂ B + _·_ : ∀ {Γ L M A B} + → Γ ⊢ L ⦂ A ⟹ B + → Γ ⊢ M ⦂ A + -------------- + → Γ ⊢ L · M ⦂ B \end{code} ## Test examples @@ -118,32 +120,31 @@ n≢m : n ≢ m n≢m () Ch : Type -Ch = (o ⇒ o) ⇒ o ⇒ o +Ch = (`ℕ ⟹ `ℕ) ⟹ `ℕ ⟹ `ℕ two : Term -two = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋)) +two = `λ s ⇒ `λ z ⇒ (` s · (` s · ` z)) ⊢two : ε ⊢ two ⦂ Ch -⊢two = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋) +⊢two = `λ `λ ` ⊢s · (` ⊢s · ` ⊢z) where ⊢s = S z≢s Z ⊢z = Z four : Term -four = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ ⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))) +four = `λ s ⇒ `λ z ⇒ ` s · (` s · (` s · (` s · ` z))) ⊢four : ε ⊢ four ⦂ Ch -⊢four = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋))) +⊢four = `λ `λ ` ⊢s · (` ⊢s · (` ⊢s · (` ⊢s · ` ⊢z))) where ⊢s = S z≢s Z ⊢z = Z plus : Term -plus = ƛ m ⦂ Ch ⇒ ƛ n ⦂ Ch ⇒ ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ - ⌊ m ⌋ · ⌊ s ⌋ · (⌊ n ⌋ · ⌊ s ⌋ · ⌊ z ⌋) +plus = `λ m ⇒ `λ n ⇒ `λ s ⇒ `λ z ⇒ ` m · ` s · (` n · ` s · ` z) -⊢plus : ε ⊢ plus ⦂ Ch ⇒ Ch ⇒ Ch -⊢plus = ƛ ƛ ƛ ƛ ⌊ ⊢m ⌋ · ⌊ ⊢s ⌋ · (⌊ ⊢n ⌋ · ⌊ ⊢s ⌋ · ⌊ ⊢z ⌋) +⊢plus : ε ⊢ plus ⦂ Ch ⟹ Ch ⟹ Ch +⊢plus = `λ `λ `λ `λ ` ⊢m · ` ⊢s · (` ⊢n · ` ⊢s · ` ⊢z) where ⊢z = Z ⊢s = S z≢s Z @@ -162,8 +163,8 @@ four′ = plus · two · two \begin{code} ⟦_⟧ᵀ : Type → Set -⟦ o ⟧ᵀ = ℕ -⟦ A ⇒ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ +⟦ `ℕ ⟧ᵀ = ℕ +⟦ A ⟹ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ ⟦_⟧ᴱ : Env → Set ⟦ ε ⟧ᴱ = ⊤ @@ -174,8 +175,8 @@ four′ = plus · two · two ⟦ S _ x ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ x ⟧ⱽ ρ ⟦_⟧ : ∀ {Γ M A} → Γ ⊢ M ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ -⟦ ⌊ x ⌋ ⟧ ρ = ⟦ x ⟧ⱽ ρ -⟦ ƛ ⊢N ⟧ ρ = λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ } +⟦ ` x ⟧ ρ = ⟦ x ⟧ⱽ ρ +⟦ `λ ⊢N ⟧ ρ = λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ } ⟦ ⊢L · ⊢M ⟧ ρ = (⟦ ⊢L ⟧ ρ) (⟦ ⊢M ⟧ ρ) _ : ⟦ ⊢four′ ⟧ tt ≡ ⟦ ⊢four ⟧ tt @@ -194,22 +195,22 @@ lookup {Γ , x ⦂ A} Z = x lookup {Γ , x ⦂ A} (S _ k) = lookup {Γ} k erase : ∀ {Γ M A} → Γ ⊢ M ⦂ A → Term -erase ⌊ k ⌋ = ⌊ lookup k ⌋ -erase (ƛ_ {x = x} {A = A} ⊢N) = ƛ x ⦂ A ⇒ erase ⊢N -erase (⊢L · ⊢M) = erase ⊢L · erase ⊢M +erase (` k) = ` lookup k +erase (`λ_ {x = x} ⊢N) = `λ x ⇒ erase ⊢N +erase (⊢L · ⊢M) = erase ⊢L · erase ⊢M \end{code} ### Properties of erasure \begin{code} -lookup-lemma : ∀ {Γ x A} → (k : Γ ∋ x ⦂ A) → lookup k ≡ x +lookup-lemma : ∀ {Γ x A} → (⊢x : Γ ∋ x ⦂ A) → lookup ⊢x ≡ x lookup-lemma Z = refl lookup-lemma (S _ k) = lookup-lemma k erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M ⦂ A) → erase ⊢M ≡ M -erase-lemma ⌊ k ⌋ = cong ⌊_⌋ (lookup-lemma k) -erase-lemma (ƛ_ {x = x} {A = A} ⊢N) = cong (ƛ x ⦂ A ⇒_) (erase-lemma ⊢N) -erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M) +erase-lemma (` ⊢x) = cong `_ (lookup-lemma ⊢x) +erase-lemma (`λ_ {x = x} ⊢N) = cong (`λ x ⇒_) (erase-lemma ⊢N) +erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M) \end{code} @@ -221,39 +222,25 @@ erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (er open Collections.CollectionDec (Id) (_≟_) \end{code} -### Properties of sets - -\begin{code} --- ⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys --- ∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys) --- []⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs --- ⊆[] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs --- bind : ∀ {x xs} → xs \\ x ⊆ xs --- left : ∀ {xs ys} → xs ⊆ xs ∪ ys --- right : ∀ {xs ys} → ys ⊆ xs ∪ ys --- prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ xs -\end{code} - ### Free variables \begin{code} free : Term → List Id -free ⌊ x ⌋ = [ x ] -free (ƛ x ⦂ A ⇒ N) = free N \\ x -free (L · M) = free L ∪ free M +free (` x) = [ x ] +free (`λ x ⇒ N) = free N \\ x +free (L · M) = free L ∪ free M \end{code} - ### Fresh identifier \begin{code} fresh : List Id → Id fresh = foldr _⊔_ 0 ∘ map suc -⊔-lemma : ∀ {x xs} → x ∈ xs → suc x ≤ fresh xs -⊔-lemma {x} {.x ∷ xs} here = m≤m⊔n (suc x) (fresh xs) -⊔-lemma {x} {y ∷ xs} (there x∈) = ≤-trans (⊔-lemma {x} {xs} x∈) - (n≤m⊔n (suc y) (fresh xs)) +⊔-lemma : ∀ {w xs} → w ∈ xs → suc w ≤ fresh xs +⊔-lemma {w} {x ∷ xs} here = m≤m⊔n (suc w) (fresh xs) +⊔-lemma {w} {x ∷ xs} (there x∈) = ≤-trans (⊔-lemma {w} {xs} x∈) + (n≤m⊔n (suc x) (fresh xs)) fresh-lemma : ∀ {x xs} → x ∈ xs → fresh xs ≢ x fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈) @@ -263,7 +250,9 @@ fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈) \begin{code} ∅ : Id → Term -∅ x = ⌊ x ⌋ +∅ x = ` x + +infixl 5 _,_↦_ _,_↦_ : (Id → Term) → Id → Term → (Id → Term) (ρ , x ↦ M) w with w ≟ x @@ -275,8 +264,8 @@ _,_↦_ : (Id → Term) → Id → Term → (Id → Term) \begin{code} subst : List Id → (Id → Term) → Term → Term -subst ys ρ ⌊ x ⌋ = ρ x -subst ys ρ (ƛ x ⦂ A ⇒ N) = ƛ y ⦂ A ⇒ subst (y ∷ ys) (ρ , x ↦ ⌊ y ⌋) N +subst ys ρ (` x) = ρ x +subst ys ρ (`λ x ⇒ N) = `λ y ⇒ subst (y ∷ ys) (ρ , x ↦ ` y) N where y = fresh ys subst ys ρ (L · M) = subst ys ρ L · subst ys ρ M @@ -291,74 +280,80 @@ N [ x := M ] = subst (free M ∪ (free N \\ x)) (∅ , x ↦ M) N \begin{code} data Value : Term → Set where - Fun : ∀ {x A N} → - -------------------- - Value (ƛ x ⦂ A ⇒ N) + Fun : ∀ {x N} + --------------- + → Value (`λ x ⇒ N) \end{code} ## Reduction \begin{code} -infix 4 _⟹_ +infix 4 _⟶_ -data _⟹_ : Term → Term → Set where +data _⟶_ : Term → Term → Set where - β-⇒ : ∀ {x A N V} → + β-⟹ : ∀ {x N V} + → Value V + ------------------------------ + → (`λ x ⇒ N) · V ⟶ N [ x := V ] + + ξ-⟹₁ : ∀ {L L′ M} + → L ⟶ L′ + ---------------- + → L · M ⟶ L′ · M + + ξ-⟹₂ : ∀ {V M M′} → Value V → - ---------------------------------- - (ƛ x ⦂ A ⇒ N) · V ⟹ N [ x := V ] - - ξ-⇒₁ : ∀ {L L′ M} → - L ⟹ L′ → + M ⟶ M′ → ---------------- - L · M ⟹ L′ · M - - ξ-⇒₂ : ∀ {V M M′} → - Value V → - M ⟹ M′ → - ---------------- - V · M ⟹ V · M′ + V · M ⟶ V · M′ \end{code} ## Reflexive and transitive closure \begin{code} -infix 2 _⟹*_ +infix 2 _⟶*_ infix 1 begin_ -infixr 2 _⟹⟨_⟩_ +infixr 2 _⟶⟨_⟩_ infix 3 _∎ -data _⟹*_ : Term → Term → Set where +data _⟶*_ : Term → Term → Set where - _∎ : ∀ {M} → - ------------- - M ⟹* M + _∎ : ∀ {M} + ------------- + → M ⟶* M - _⟹⟨_⟩_ : ∀ (L : Term) {M N} → - L ⟹ M → - M ⟹* N → - --------- - L ⟹* N + _⟶⟨_⟩_ : ∀ (L : Term) {M N} + → L ⟶ M + → M ⟶* N + --------- + → L ⟶* N -begin_ : ∀ {M N} → (M ⟹* N) → (M ⟹* N) -begin M⟹*N = M⟹*N +begin_ : ∀ {M N} → (M ⟶* N) → (M ⟶* N) +begin M⟶*N = M⟶*N \end{code} ## Progress \begin{code} data Progress (M : Term) : Set where - step : ∀ {N} → M ⟹ N → Progress M - done : Value M → Progress M + step : ∀ {N} + → M ⟶ N + ---------- + → Progress M + done : + Value M + ---------- + → Progress M progress : ∀ {M A} → ε ⊢ M ⦂ A → Progress M -progress ⌊ () ⌋ -progress (ƛ_ ⊢N) = done Fun +progress (` ()) +progress (`λ_ ⊢N) = done Fun progress (⊢L · ⊢M) with progress ⊢L -... | step L⟹L′ = step (ξ-⇒₁ L⟹L′) +... | step L⟶L′ = step (ξ-⟹₁ L⟶L′) ... | done Fun with progress ⊢M -... | step M⟹M′ = step (ξ-⇒₂ Fun M⟹M′) -... | done valM = step (β-⇒ valM) +... | step M⟶M′ = step (ξ-⟹₂ Fun M⟶M′) +... | done valM = step (β-⟹ valM) \end{code} @@ -376,10 +371,10 @@ dom-lemma Z = here dom-lemma (S x≢y ⊢y) = there (dom-lemma ⊢y) free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ -free-lemma ⌊ ⊢x ⌋ w∈ with w∈ -... | here = dom-lemma ⊢x +free-lemma (` ⊢x) w∈ with w∈ +... | here = dom-lemma ⊢x ... | there () -free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N) = proj₂ lemma-\\-∷ (free-lemma ⊢N) +free-lemma {Γ} (`λ_ {x = x} {N = N} ⊢N) = proj₂ lemma-\\-∷ (free-lemma ⊢N) free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈ ... | inj₁ ∈L = free-lemma ⊢L ∈L ... | inj₂ ∈M = free-lemma ⊢M ∈M @@ -388,13 +383,15 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈ ### Renaming \begin{code} -⊢rename : ∀ {Γ Δ xs} → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) → - (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) -⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋) = ⌊ ⊢σ ∈xs ⊢x ⌋ +⊢rename : ∀ {Γ Δ xs} + → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) + -------------------------------------------------- + → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) +⊢rename ⊢σ ⊆xs (` ⊢x) = ` ⊢σ ∈xs ⊢x where ∈xs = proj₂ lemma-[_] ⊆xs -⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N) - = ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) +⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N) + = `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) where Γ′ = Γ , x ⦂ A Δ′ = Δ , x ⦂ A @@ -407,7 +404,7 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈ ... | there ∈xs = S x≢y (⊢σ ∈xs ⊢y) ⊆xs′ : free N ⊆ xs′ - ⊆xs′ = proj₁ lemma-\\-∷ ⊆xs + ⊆xs′ = proj₁ lemma-\\-∷ ⊆xs ⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M) = ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M where @@ -426,21 +423,22 @@ lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs lemma₂ x≢ here = ⊥-elim (x≢ refl) lemma₂ _ (there w∈) = w∈ -⊢subst : ∀ {Γ Δ xs ys ρ} → - (∀ {x} → x ∈ xs → free (ρ x) ⊆ ys) → - (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) → - (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ A) -⊢subst Σ ⊢ρ ⊆xs ⌊ ⊢x ⌋ +⊢subst : ∀ {Γ Δ xs ys ρ} + → (∀ {x} → x ∈ xs → free (ρ x) ⊆ ys) + → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) + ------------------------------------------------------------- + → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ A) +⊢subst Σ ⊢ρ ⊆xs (` ⊢x) = ⊢ρ (⊆xs here) ⊢x -⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N) - = ƛ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N) +⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N) + = `λ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N) where y = fresh ys Γ′ = Γ , x ⦂ A Δ′ = Δ , y ⦂ A xs′ = x ∷ xs ys′ = y ∷ ys - ρ′ = ρ , x ↦ ⌊ y ⌋ + ρ′ = ρ , x ↦ ` y Σ′ : ∀ {w} → w ∈ xs′ → free (ρ′ w) ⊆ ys′ Σ′ {w} here with w ≟ x @@ -458,7 +456,7 @@ lemma₂ _ (there w∈) = w∈ ⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C ⊢ρ′ _ Z with x ≟ x - ... | yes _ = ⌊ Z ⌋ + ... | yes _ = ` Z ... | no x≢x = ⊥-elim (x≢x refl) ⊢ρ′ {w} w∈′ (S x≢w ⊢w) with w ≟ x ... | yes refl = ⊥-elim (x≢w refl) @@ -499,7 +497,7 @@ lemma₂ _ (there w∈) = w∈ ... | no x≢x = ⊥-elim (x≢x refl) ⊢ρ {z} z∈ (S x≢z ⊢z) with z ≟ x ... | yes refl = ⊥-elim (x≢z refl) - ... | no _ = ⌊ ⊢z ⌋ + ... | no _ = ` ⊢z ⊆xs : free N ⊆ xs ⊆xs x∈ = x∈ @@ -508,12 +506,16 @@ lemma₂ _ (there w∈) = w∈ ### Preservation \begin{code} -preservation : ∀ {Γ M N A} → Γ ⊢ M ⦂ A → M ⟹ N → Γ ⊢ N ⦂ A -preservation ⌊ ⊢x ⌋ () -preservation (ƛ ⊢N) () -preservation (⊢L · ⊢M) (ξ-⇒₁ L⟹L′) = preservation ⊢L L⟹L′ · ⊢M -preservation (⊢V · ⊢M) (ξ-⇒₂ valV M⟹M′) = ⊢V · preservation ⊢M M⟹M′ -preservation ((ƛ ⊢N) · ⊢W) (β-⇒ valW) = ⊢substitution ⊢N ⊢W +preservation : ∀ {Γ M N A} + → Γ ⊢ M ⦂ A + → M ⟶ N + --------- + → Γ ⊢ N ⦂ A +preservation (` ⊢x) () +preservation (`λ ⊢N) () +preservation (⊢L · ⊢M) (ξ-⟹₁ L⟶L′) = preservation ⊢L L⟶L′ · ⊢M +preservation (⊢V · ⊢M) (ξ-⟹₂ valV M⟶M′) = ⊢V · preservation ⊢M M⟶M′ +preservation ((`λ ⊢N) · ⊢W) (β-⟹ valW) = ⊢substitution ⊢N ⊢W \end{code}