For the sake of the following proofs we consider ⟨⟩ a degenerate case of the pair construct and we’ll omit the correspondent cases. We give the definition of substitution for the new constructs;

[e/x]inl^{τ_{1}+τ_{2}}e = inl^{τ_{1}+τ_{2}}[e/x]e
[e/x]inr^{τ_{1}+τ_{2}}e = inr^{τ_{1}+τ_{2}}[e/x]e
[e/x]case e of x_{1}:τ_{1} ⇒ e_{1} | x_{2}:τ_{2} ⇒ e_{2} = case e of x_{1}:τ_{1} ⇒ e_{1} | x_{2}:τ_{2} ⇒ e_{2}

if x ∈ {x_{1}, x_{2}}

= case e of x_{1}:τ_{1} ⇒ e_{1} | x_{2}:τ_{2} ⇒ [e/x]e_{2}

if x = x_{1}

= case e of x_{1}:τ_{1} ⇒ [e/x]e_{1} | x_{2}:τ_{2} ⇒ e_{2}

if x = x_{2}

= case [e/x]e of x_{1}:τ_{1} ⇒ [e/x]e_{1} | x_{2}:τ_{2} ⇒ [e/x]e_{2}

otherwise

[e/x]⟨e_{1}, e_{2}⟩ = ⟨[e/x]e_{1}⟩[e/x]e_{2}
[e/x]bind p to e_{1} in e_{2} = bind p to [e/x]e_{1} in e_{2}

if x ∈ F V (p)

[e/x]bind p to e_{1} in e_{2} = bind p to [e/x]e_{1} in [e/x]e_{2}

otherwise

Lemma 1 (Substitution for sums and products) If Γ[x:τ] ⊢ e′ : τ′ and Γ ⊢ e : τ, then Γ ⊢ [e/x]e′ : τ′.

Proof: By induction on the structure of the derivation of Γ[x:τ] ⊢ e′ : τ′;

PairType e′ = ⟨e_{1}, e_{2}⟩ and τ′ = τ_{1} ∗ τ_{2}. By subderivations Γ[x:τ] ⊢ e_{1} : τ_{1} and Γ[x:τ] ⊢ e_{2} : τ_{2}; by IH Γ ⊢ [e/x]e_{1} : τ_{1} and Γ ⊢ [e/x]e_{2} : τ_{2} and by the typing rule Γ ⊢ ⟨[e/x]e_{1}, [e/x]e_{2}⟩ : τ_{1} ∗ τ_{2}. By definition of substitution Γ ⊢ [e/x]⟨e_{1}, e_{2}⟩ : τ_{1} ∗ τ_{2} as required.

InlType e′ = inl^{τ_{1}+τ_{2}}e_{1} and τ′ = τ_{+}τ_{2}. By subderivations Γ[x:τ] ⊢ e_{1} : τ_{1} ; by IH Γ ⊢ [e/x]e_{1} : τ_{1} and by the typing rule Γ ⊢ inl^{τ_{1}+τ_{2}}[e/x]e_{1} : τ_{1} + τ_{2}. By definition of substitution Γ ⊢ [e/x]inl^{τ_{1}+τ_{2}}e_{1} : τ_{1} + τ_{2} as required.

InrType e′ = inr^{τ_{1}+τ_{2}}e_{1} and τ′ = τ_{1} + τ_{2}. Symmetrical.

CaseType e′ = case e′′ of inl x_{1} : τ_{1} ⇒ e_{1} | inr x_{2} : τ_{2} ⇒ e_{2} and τ′ = τ′′. By reneaming we can choose x_{1}, x_{2} such that

{x_{1}, x_{2}} ∩ (F V (e) ∪ {x} ∪ dom(Γ)) = ∅

By sub-derivation Γ[x:τ] ⊢ e′′ : τ_{1} + τ_{2}, Γ[x_{1}:τ_{1}] ⊢ e_{1} : τ_{1} and Γ[x_{2}:τ_{2}] ⊢ e_{2} : τ_{2}. By IH Γ ⊢ [e/x]e′′ : τ_{1} + τ_{2}, Γ[x_{1}:τ_{1}] ⊢ [e/x]e_{1} : τ_{1} and Γ[x_{2}:τ_{2}] ⊢ [e/x]e_{2} : τ_{2}; by rule Γ ⊢ case [e/x]e′′ of x_{1} ⇒ [e/x]e_{1} | x_{2} ⇒ [e/x]e_{2} and by substitution Γ ⊢ [e/x]case e′′ of inl x_{1} : τ_{1} ⇒ e_{1} | inr x_{2} : τ_{2} ⇒ e_{2} : τ′′ as required.

BindType e′ = bind p to e_{1} in e_{2} and τ′ = τ′′. By renaming we can choose p such

that

F V (p) ∩ (F V (e) ∪ {x} ∪ dom(Γ)) = ∅

By sub-derivations Γ[x:τ] ⊢ e_{1} : τ_{1}, Γ[x:τ] ⊢ p : τ_{1} ↪ Γ′ and Γ′ ⊢ e_{2} : τ_{2}. By IH Γ ⊢ [e/x]e_{1} : τ_{1}. By weakening Γ′ ⊢ e : τ. By IH Γ′ ⊢ [e/x]e_{2} : τ_{2}. By strengthening extended to the patterm judgment, as x ∉ F V (p) Γ ⊢ p : τ_{1} ↪ Γ′. By rule Γ ⊢ bind p to [e/x]e_{1} in [e/x]e_{2} : τ′′ and by substitution Γ ⊢ [e/x]bind p to e_{1} in e_{2} : τ′′ as required.

□

Lemma 2 (Canonical Forms for sums and products) If v is a closed well formed value of type τ, then:

1. If τ = τ_{1} ∗ τ_{2}, then v = ⟨v_{1}, v_{2}⟩.

2. If τ = τ_{1} + τ_{2}, then v = inl^{τ_{1}+τ_{2}}v′ or v = inr^{τ_{1}+τ_{2}}v′.

Proof: By induction on the typing judgment, exploiting the definition of value.

1. Assume τ = τ1 ∗ τ_{2} and v : τ; by inversion on the typing rule v = ⟨v_{1}, v_{2}⟩ and there is v_{i} : τ_{i} for i = 1, 2. By induction hypothesis v_{i} is a value. Thus by definition of value ⟨v1, v2⟩ is a value. As a special case if τ = 1, then v = ⟨⟩.

2. Assume τ = τ1 + τ_{2} and v : τ; by inversion on the typing rule either v = inl^{τ_{1}+τ_{2}}v′ and v′ : τ_{2} or v = inr^{τ_{1}+τ_{2}}v′ and v′ : τ_{2}. In both cases, by induction hypothesis v′ is a value. Thus by definition of value either inl^{τ_{1}+τ_{2}}v′ or inr^{τ_{1}+τ_{2}}v′ is a value.

□

Lemma 3 (Canonical Forms for recursive types) If v′ is a value of type μα. τ, then v′ = fold ^{μα. τ} v.

Proof: By induction on the typing judgment, exploiting the definition of value.

1. Assume v′ : μα. τ; by inversion on the typing rule v′ = fold^{μα. τ} v and there is v : [μα. τ/α]τ. By induction hypothesis v is a value. Thus by definition of value fold^{μα. τ} v is a value.

□

The Substitution Lemma for terms is by now, straightforward.

Theorem 4 (Preservation for recursive types) Assume e ↦ e′; then if e : τ, then e′ : τ.

Proof: By induction on the evaluation rules:

FoldTest e = fold^{μα. τ} e_{1} and e′ = e′_{1}. By inversion e_{1} : [μα. τ/α]τ. By IH e′_{1} : [μα. τ/α]τ and by rule fold^{μα. τ} e′_{1} : μα. τ.

UnFoldTest e = unfold e_{1} and e′ = e′_{1}. By inversion e_{1} : μα. τ. By IH e′_{1} : μα. τ and by rule unfold e′_{1} : [μα. τ/α]τ.

FoldBeta e = unfold (fold^{μα. τ} v) and e′ = v, where τ = [μα. τ/α]τ. By inversion fold^{μα. τ} v : μα. τ; by inversion again e : [μα. τ/α]τ as required.

□

Theorem 5 (Progress for recursive types) If e : τ, then either e is a value or there is e′ such that e ↦ e′.

Proof: By induction on the typing rules.

TypeFold e = fold^{μα. τ_{1}}e_{1} and τ = μα. τ_{1}. By IH either e_{1} is a value or there is e′_{1} such that e_{1} ↦ e′_{1}. Subcase e_{1} is a value; then by definition of value e = fold^{μα. τ_{1}}e_{1} is a value. Subcase e_{1} ↦ e′_{1}; by rule F oldT est fold^{μα. τ_{1}}e_{1} ↦ fold^{μα. τ_{1}}e′_{1}.

TypeUnfold e = unfold e_{1} and τ = [μα. τ_{1}/α]τ. By IH either e_{1} is a value or there is e′_{1} such that e_{1} ↦ e′_{1}. Subcase e_{1} is a value; then by the Canonical Form lemma e = fold^{μα. τ_{1}}v; by rule F oldBeta unfold (fold^{μα. τ_{1}}v) ↦ v. Subcase e_{1} ↦ e′_{1}; by rule UnfoldT est unfold e_{1} ↦ unfold e′_{1}.

□