diff --git a/prototyping/Luau/TypeNormalization.agda b/prototyping/Luau/TypeNormalization.agda
index e90090c1..098021fb 100644
--- a/prototyping/Luau/TypeNormalization.agda
+++ b/prototyping/Luau/TypeNormalization.agda
@@ -9,6 +9,7 @@ _∩ⁿˢ_ : Type → Type → Type
 _∪ⁿ_ : Type → Type → Type
 _∩ⁿ_ : Type → Type → Type
 _⇒ⁿ_ : Type → Type → Type
+tgtⁿ : Type → Type → Type
 
 -- Union of function types
 (F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G)
@@ -54,8 +55,10 @@ unknown ∪ⁿˢ T = unknown
 F ∪ⁿˢ T = F ∪ T
 
 -- Functions on normalized types
-never ⇒ⁿ T = never ⇒ unknown
-S ⇒ⁿ T = S ⇒ T
+S ⇒ⁿ T = S ⇒ (tgtⁿ S T)
+
+tgtⁿ never T = unknown
+tgtⁿ S T = T
 
 -- Normalize!
 normalize : Type → Type
diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda
index 972b14a2..f698642a 100644
--- a/prototyping/Properties/Subtyping.agda
+++ b/prototyping/Properties/Subtyping.agda
@@ -165,6 +165,12 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T)
 <:-∩-symm t (p₁ , p₂) = (p₂ , p₁)
 
+<:-∩-assocl : ∀ {S T U} → (S ∩ (T ∩ U)) <: ((S ∩ T) ∩ U)
+<:-∩-assocl t (p , (p₁ , p₂)) = (p , p₁) , p₂
+
+<:-∩-assocr : ∀ {S T U} → ((S ∩ T) ∩ U) <: (S ∩ (T ∩ U))
+<:-∩-assocr t ((p , p₁) , p₂) = p , (p₁ , p₂)
+
 ≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U))
 ≮:-∩-left (witness t p q) = witness t p (left q)
 
@@ -206,6 +212,9 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 ∪-distr-∩-<: t (left p₁ , right p₂) = right p₂
 ∪-distr-∩-<: t (right p₁ , p₂) = right p₁
 
+∩-<:-∪ : ∀ {S T} → (S ∩ T) <: (S ∪ T)
+∩-<:-∪ t (p , _) = left p
+
 -- Properties of functions
 <:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U)
 <:-function p q function function = function
diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda
index 14190173..3307d0a9 100644
--- a/prototyping/Properties/TypeNormalization.agda
+++ b/prototyping/Properties/TypeNormalization.agda
@@ -4,7 +4,7 @@ module Properties.TypeNormalization where
 
 open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
 open import Luau.Subtyping using (Tree; Language; function; scalar; unknown; right; scalar-function-err; _,_)
-open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; _⇒ⁿ_; normalize)
+open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; _⇒ⁿ_; tgtⁿ; normalize)
 open import Luau.Subtyping using (_<:_)
 open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect;  ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never; <:-function-never)
 
@@ -237,6 +237,17 @@ scalar-∩-fun-<:-never function S = scalar-∩-function-<:-never S
 scalar-∩-fun-<:-never (T ⇒ U) S = scalar-∩-function-<:-never S
 scalar-∩-fun-<:-never (F ∩ G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S)
 
+<:-tgtⁿ : ∀ {S T U} → (T <: U) → T <: tgtⁿ S U
+<:-tgtⁿ {never} p = <:-unknown
+<:-tgtⁿ {nil} p = p
+<:-tgtⁿ {unknown} p = p
+<:-tgtⁿ {boolean} p = p
+<:-tgtⁿ {number} p = p
+<:-tgtⁿ {string} p = p
+<:-tgtⁿ {S ⇒ T} p = p
+<:-tgtⁿ {S ∪ T} p = p
+<:-tgtⁿ {S ∩ T} p = p
+
 flipper : ∀ {S T U} → ((S ∪ T) ∪ U) <: ((S ∪ U) ∪ T)
 flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪-assocl)