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; first we extend the notion of free variables as follows:

F V (inl^{τ_{1}+τ_{2}}e) = F V (e)
F V (inr^{τ_{1}+τ_{2}}e) = F V (e)
F V (case e of x_{1}:τ_{1} ⇒ e_{1} | x_{2}:τ_{2} ⇒ e_{2}) = F V (e) ∪ (F V (e_{1}) \ {x_{1}}) ∪ (F V (e_{2}) \ {x_{2}})
F V (⟨e_{1}, e_{2}⟩) = F V (e_{1}) ∪ F V (e_{2})
F V (bind p to e_{1} in e_{2}) = F V (e_{1}) ∪ (F V (e_{2}) \ F V (p))
F V ( ) = ∅
F V (x:τ) = {x}
F V (⟨p_{1}, p_{2}⟩) = F V (p_{1}) ∪ F V (p_{2})

[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

We will need the following auxiliary Lemma.

Lemma 0.1 (Strengthening for patterns) If Γ[x:τ] ⊢ p′ : τ′ ↪ Γ′ and x ∉ F V (p), then Γ ⊢ p′ : τ′ ↪ Γ′.

Proof: By induction on the structure of the given derivation. □

Lemma 0.2 (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 : τ and Γ′[x:τ] ⊢ e_{2} : τ. By IH Γ′ ⊢ [e/x]e_{2} : τ_{2}. By strengthening, 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 0.3 (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 inspection of the the typing judgment, noting that for each value only one typing rule applies. □