On page 4, the term
   λx.δ[π₂x|x₁.ι₁⟨π₁x,x₁⟩|x₂.ι₂⟨π₁x₁,ι₂π₂x₁⟩]
should be
   λx.δ[π₂x|x₁.ι₁⟨π₁x,x₁⟩|x₂.ι₂⟨π₁x,x₂⟩].