**Exercise 22.3.9**: For clarity, the original constraint typing rules from class are reproduced below.

```
┌──────────────────┐
│ Γ ⊢ t : T | V; C │
└──────────────────┘

x : T ∈ Γ
---------------- CT-Var
Γ ⊢ x : T | ∅, ∅

Γ, x : T₁ ⊢ t₂ : T₂ | V; C
-------------------------------- CT-Abs
Γ ⊢ λx : T₁. t₂ : T₁ → T₂ | V; C

Γ ⊢ t₁ : T₁ | V₁; C₁
Γ ⊢ t₂ : T₂ | V₂; C₂
V₁ ∩ V₂ = V₁ ∩ FV(T₂) = V₂ ∩ FV(T₁) = ∅
X ∉ V₁, V₂, FV(T₁, T₂, C₁, C₂, Γ, t₁, t₂)
------------------------------------------------------ CT-App
Γ ⊢ t₁ t₂ : X | V₁ ∪ V₂ ∪ {X}; C₁ ∪ C₂ ∪ {T₁ = T₂ → X}
```

The new constraint typing rules that thread through unused type variables are below.

```
┌─────────────────────┐
│ Γ; F ⊢ t : T | F; C │
└─────────────────────┘

x : T ∈ Γ
------------------- FCT-Var
Γ; F ⊢ x : T | F; ∅

Γ, x : T₁; F ⊢ t₂ : T₂ | F'; C
------------------------------------ FCT-Abs
Γ; F ⊢ λx : T₁. t₂ : T₁ → T₂ | F'; C

Γ; F₁ ⊢ t₁ : T₁ | F₂; C₁
Γ; F₂ ⊢ t₂ : T₂ | F₃; C₂
X ∈ F₃    F₄ = F₃ \ {X}
----------------------------------------------------- FCT-App
Γ; F₁ ⊢ t₁ t₂ : X | F₄; C₁ ∪ C₂ ∪ {T₁ = T₂ → X}
```

A key property of the new rules is that the output variables
are indeed fresh with respect to the inputs and the other outputs.

**Lemma**: If Γ; Fᵢ ⊢ t : T | Fₒ; C and Fᵢ ∩ (FV(Γ) ∪ FV(t)) = ∅ then Fₒ ⊆ Fᵢ and Fₒ ∩ (FV(T) ∪ FV(C)) = ∅.
**Proof**: By induction on the derivation of the new typing rules.
* Case FCT-Var (F₀ = Fᵢ = F): F ∩ FV(Γ) = ∅ and x : T ∈ Γ so F ∩ FV(T) = ∅.
* Case FCT-Abs: By supposition, F ∩ FV(T₁) = ∅. 
  Then by the induction hypothesis, F' ⊆ F and F' ∩ (FV(T₂) ∪ FV(C)) = ∅,
  and we also have F ∩ FV(T₁) = ∅ by the supposition and by subset,
  so we have F ∩ FV(T₁ → T₂) = ∅ as needed.
* Case FCT-App: By supposition, F₁ ∩ FV(t₁) = F₁ ∩ FV(t₂) = ∅.
  By the induction hypothesis on both premises in sequence,
  we have F₃ ⊆ F₂ ⊆ F₁ and F₂ ∩ (FV(T₁) ∪ FV(C₁)) = F₃ ∩ (FV(T₂) ∪ FV(C₂)) = ∅.
  By definition, F₄ ⊆ F₃, and X ∉ F₄.
  Then F₄ ∩ (FV(T₁) ∪ FV(T₂) ∪ FV(C₁) ∪ FV(C₂)) = ∅ by subset,
  so F₄ ∩ (FV(C₁ ∪ C₂ ∪ {T₁ = T₂ → X})) - ∅ as well.

We can then show that the typing judgements imply one another.

**Lemma** (soundness of FCT wrt CT): Suppose Fᵢ ∩ (FV(Γ) ∪ FV(t)) = ∅.
If Γ; Fᵢ ⊢ t : T | Fₒ : C, then Γ ⊢ t : T | Fᵢ \ Fₒ; C.
**Proof**: By induction on the derivation of the new typing rules.
* Case FCT-App: The premises are Γ; F₁ ⊢ t₁ : T₁ | F₂; C₁ and Γ; F₂ ⊢ t₂ : T₂ | F₃; C₂,
  along with X ∈ F₃ and F₄ = F₃ \ {X}.
  The goal is to show that Γ ⊢ t : T | F₁ \ F₄; C₁ ∪ C₂ ∪ {T₁ = T₂ → X}.
  Applying CT-App, we need the following premises:
    1. Γ ⊢ t₁ : T₁ | V₁; C₁ for some V₁;
    2.  Γ ⊢ t₂ : T₂ | V₂; C₂ for some V₂;
    3.  V₁ ∩ V₂ = V₁ ∩ FV(T₂) = V₂ ∩ FV(T₁) = ∅; and
    4. X ∉ V₁, V₂, FV(T₁, T₂, C₁, C₂, Γ, t₁, t₂).
    By the induction hypothesis, we have the first goal where V₁ = F₁ \ F₂.
    By the above lemma, F₂ ⊆ F₁, so its variables are not free in Γ or t₂.
    Then we apply the induction hypothesis again to yield the second goal where V₂ = F₂ \ F₃.
    By set subtraction, we know that V₁ ∩ V₂ = ∅.

**Lemma** (completeness of FCT wrt CT): V ∩ (FV(Γ) ∪ FV(t)) = ∅.
If Γ ⊢ t : T | V; C, then Γ; V ⊢ t : T | {}; C.