diff --git a/prototyping/Luau/StrictMode/ToString.agda b/prototyping/Luau/StrictMode/ToString.agda
index dd99f4ee..7c5f0253 100644
--- a/prototyping/Luau/StrictMode/ToString.agda
+++ b/prototyping/Luau/StrictMode/ToString.agda
@@ -4,7 +4,7 @@ module Luau.StrictMode.ToString where
 
 open import Agda.Builtin.Nat using (Nat; suc)
 open import FFI.Data.String using (String; _++_)
-open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err)
+open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err; function-tgt)
 open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
 open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
 open import Luau.Type using (number; boolean; string; nil)
@@ -29,6 +29,7 @@ treeToString (scalar nil) n v = v ++ " is nil"
 treeToString function n v = v ++ " is a function"
 treeToString (function-ok s t) n v = treeToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n  " ++ treeToString s (suc n) w where w = tmp n
 treeToString (function-err t) n v = v ++ "(" ++ w ++ ") can error when\n  " ++ treeToString t (suc n) w where w = tmp n
+treeToString (function-tgt t) n v = treeToString t n (v ++ "()")
 
 subtypeWarningToString : ∀ {T U} → (T ≮: U) → String
 subtypeWarningToString (witness t p q) = "\n  because provided type contains v, where " ++ treeToString t 0 "v"
diff --git a/prototyping/Luau/Subtyping.agda b/prototyping/Luau/Subtyping.agda
index 0b7f3c3f..dc2abed0 100644
--- a/prototyping/Luau/Subtyping.agda
+++ b/prototyping/Luau/Subtyping.agda
@@ -15,6 +15,7 @@ data Tree : Set where
   function : Tree
   function-ok : Tree → Tree → Tree
   function-err : Tree → Tree
+  function-tgt : Tree → Tree
 
 data Language : Type → Tree → Set
 data ¬Language : Type → Tree → Set
@@ -26,6 +27,7 @@ data Language where
   function-ok₁ : ∀ {T U t u} → (¬Language T t) → Language (T ⇒ U) (function-ok t u)
   function-ok₂ : ∀ {T U t u} → (Language U u) → Language (T ⇒ U) (function-ok t u)
   function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
+  function-tgt : ∀ {T U t} → (Language U t) → Language (T ⇒ U) (function-tgt t)
   left : ∀ {T U t} → Language T t → Language (T ∪ U) t
   right : ∀ {T U u} → Language U u → Language (T ∪ U) u
   _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
@@ -37,9 +39,11 @@ data ¬Language where
   scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
   scalar-function-ok : ∀ {S t u} → (Scalar S) → ¬Language S (function-ok t u)
   scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
+  scalar-function-tgt : ∀ {S t} → (Scalar S) → ¬Language S (function-tgt t)
   function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
   function-ok : ∀ {T U t u} → (Language T t) → (¬Language U u) → ¬Language (T ⇒ U) (function-ok t u)
   function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)
+  function-tgt : ∀ {T U t} → (¬Language U t) → ¬Language (T ⇒ U) (function-tgt t)
   _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
   left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
   right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u
diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda
index bf194930..503838f9 100644
--- a/prototyping/Properties/DecSubtyping.agda
+++ b/prototyping/Properties/DecSubtyping.agda
@@ -5,13 +5,13 @@ module Properties.DecSubtyping where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
-open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
 open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
 open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
 open import Luau.TypeSaturation using (saturate)
 open import Properties.Contradiction using (CONTRADICTION; ¬)
 open import Properties.Functions using (_∘_)
-open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub;  ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb;  ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right; <:-impl-¬≮:; <:-intersect; <:-function-∩-∪; <:-function-∩; <:-function-never; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp)
+open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub;  ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb;  ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right; <:-impl-¬≮:; <:-intersect; <:-function-∩-∪; <:-function-∩; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp)
 open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalᶠ; function-top)
 open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; defn; here; left; right; ov-language; ov-<:; saturated; normal-saturate; normal-overload-src; normal-overload-tgt; saturate-<:; <:-saturate; <:ᵒ-impl-<:; _>>=ˡ_; _>>=ʳ_)
 open import Properties.Equality using (_≢_)
@@ -25,12 +25,13 @@ fun-¬scalar s (S ⇒ T) function = scalar-function s
 fun-¬scalar s (S ⇒ T) (function-ok₁ p) = scalar-function-ok s
 fun-¬scalar s (S ⇒ T) (function-ok₂ p) = scalar-function-ok s
 fun-¬scalar s (S ⇒ T) (function-err p) = scalar-function-err s
+fun-¬scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
 fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂
 
 -- Honest this terminates, since saturation maintains the depth of nested arrows
 {-# TERMINATING #-}
 dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
-dec-subtypingˢᶠᵒ : ∀ {F S T} → FunType F → Saturated F → FunType (S ⇒ T) → (S ≮: never) → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
+dec-subtypingˢᶠᵒ : ∀ {F S T} → FunType F → Saturated F → FunType (S ⇒ T) → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
 dec-subtypingˢᶠ : ∀ {F G} → FunType F → Saturated F → FunType G → Either (F ≮: G) (F <: G)
 dec-subtypingᶠ : ∀ {F G} → FunType F → FunType G → Either (F ≮: G) (F <: G)
 dec-subtypingᶠⁿ : ∀ {F U} → FunType F → Normal U → Either (F ≮: U) (F <: U)
@@ -41,7 +42,7 @@ dec-subtypingˢⁿ T U with dec-language _ (scalar T)
 dec-subtypingˢⁿ T U | Left p = Left (witness (scalar T) (scalar T) p)
 dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)
 
-dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) (witness s₀ Ss₀ never) = result (top Fᶠ (λ o → o)) where
+dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) = result (top Fᶠ (λ o → o)) where
 
   data Top G : Set where
 
@@ -100,7 +101,7 @@ dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) (w
          })
 
     result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
-    result₀ (no S₀ T₀ o₀ (witness t T₀t ¬Tt) tgt₀) = Left (witness (function-ok s₀ t) (ov-language Fᶠ (λ o → function-ok₂ (tgt₀ o t T₀t))) (function-ok Ss₀ ¬Tt))
+    result₀ (no S₀ T₀ o₀ (witness t T₀t ¬Tt) tgt₀) = Left (witness (function-tgt t) (ov-language Fᶠ (λ o → function-tgt (tgt₀ o t T₀t))) (function-tgt ¬Tt))
     result₀ (yes S₀ T₀ o₀ T₀<:T src₀) with dec-subtypingⁿ Sⁿ (normal-overload-src Fᶠ o₀)
     result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right (defn o₀ S<:S₀ T₀<:T)
     result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Left (witness s Ss ¬S₀s) = Left (result₁ (smallest Fᶠ (λ o → o))) where
@@ -136,11 +137,9 @@ dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) (w
         lemma {S′} o | Left ¬S′s = function-ok₁ ¬S′s
         lemma {S′} o | Right S′s = function-ok₂ (tgt₁ o S′s t T₁t)
 
-dec-subtypingˢᶠ F Fˢ (S ⇒ T) with dec-subtypingⁿ S never
-dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Right S<:never = Right (<:-trans (function-top F) (<:-trans <:-function-never (<:-function S<:never <:-refl)))
-dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left S≮:never with dec-subtypingˢᶠᵒ F Fˢ (S ⇒ T) S≮:never
-dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left S≮:never | Left F≮:S⇒T = Left F≮:S⇒T
-dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left S≮:never | Right F<:ᵒS⇒T = Right (<:ᵒ-impl-<: F F<:ᵒS⇒T)
+dec-subtypingˢᶠ F Fˢ (S ⇒ T) with dec-subtypingˢᶠᵒ F Fˢ (S ⇒ T) 
+dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left F≮:S⇒T = Left F≮:S⇒T
+dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Right F<:ᵒS⇒T = Right (<:ᵒ-impl-<: F F<:ᵒS⇒T)
 dec-subtypingˢᶠ F Fˢ (G ∩ H) with dec-subtypingˢᶠ F Fˢ G | dec-subtypingˢᶠ F Fˢ H
 dec-subtypingˢᶠ F Fˢ (G ∩ H) | Left F≮:G | _ = Left (≮:-∩-left F≮:G)
 dec-subtypingˢᶠ F Fˢ (G ∩ H) | _ | Left F≮:H = Left (≮:-∩-right F≮:H)
@@ -186,7 +185,7 @@ dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (norm
 -- <:ᵒ coincides with <:, that is F is a subtype of (S ⇒ T) precisely
 -- when one of its overloads is.
 
-<:-impl-<:ᵒ : ∀ {F S T} → FunType F → Saturated F → (S ≮: never) → (F <: (S ⇒ T)) → (F <:ᵒ (S ⇒ T))
-<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ S≮:never F<:S⇒T with dec-subtypingˢᶠᵒ Fᶠ Fˢ (normal S ⇒ normal T) (<:-trans-≮: (<:-normalize S) S≮:never)
-<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ S≮:never F<:S⇒T | Left F≮:S⇒T = CONTRADICTION (<:-impl-¬≮: (<:-trans F<:S⇒T (<:-normalize (S ⇒ T))) F≮:S⇒T)
-<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ S≮:never F<:S⇒T | Right F<:ᵒS⇒T = F<:ᵒS⇒T >>=ˡ <:-normalize S >>=ʳ normalize-<: T
+<:-impl-<:ᵒ : ∀ {F S T} → FunType F → Saturated F → (F <: (S ⇒ T)) → (F <:ᵒ (S ⇒ T))
+<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ F<:S⇒T with dec-subtypingˢᶠᵒ Fᶠ Fˢ (normal S ⇒ normal T)
+<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ F<:S⇒T | Left F≮:S⇒T = CONTRADICTION (<:-impl-¬≮: (<:-trans F<:S⇒T (<:-normalize (S ⇒ T))) F≮:S⇒T)
+<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ F<:S⇒T | Right F<:ᵒS⇒T = F<:ᵒS⇒T >>=ˡ <:-normalize S >>=ʳ normalize-<: T
diff --git a/prototyping/Properties/FunctionTypes.agda b/prototyping/Properties/FunctionTypes.agda
index 50db27c7..794e5b3f 100644
--- a/prototyping/Properties/FunctionTypes.agda
+++ b/prototyping/Properties/FunctionTypes.agda
@@ -4,7 +4,7 @@ module Properties.FunctionTypes where
 
 open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
 open import Luau.FunctionTypes using (srcⁿ; src; tgt)
-open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
 open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
 open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
 open import Properties.Functions using (_∘_)
@@ -65,6 +65,7 @@ fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S)
 ¬fun-scalar s (S ⇒ T) (function-ok₁ p) = scalar-function-ok s
 ¬fun-scalar s (S ⇒ T) (function-ok₂ p) = scalar-function-ok s
 ¬fun-scalar s (S ⇒ T) (function-err p) = scalar-function-err s
+¬fun-scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
 ¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂
 
 fun-function : ∀ {T} → FunType T → Language T function
@@ -114,3 +115,4 @@ unknown-src-≮: r (witness (function-ok s .function) p (function-ok x (scalar-f
 unknown-src-≮: r (witness (function-ok s .(function-ok _ _)) p (function-ok x (scalar-function-ok ())))
 unknown-src-≮: r (witness (function-ok s .(function-err _)) p (function-ok x (scalar-function-err ())))
 unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
+unknown-src-≮: r (witness (function-tgt t) p (function-tgt (scalar-function-tgt ())))
diff --git a/prototyping/Properties/ResolveOverloads.agda b/prototyping/Properties/ResolveOverloads.agda
index 82a9971f..a2f30eee 100644
--- a/prototyping/Properties/ResolveOverloads.agda
+++ b/prototyping/Properties/ResolveOverloads.agda
@@ -74,22 +74,22 @@ resolve F R = resolveⁿ (normal F) (normal R)
 <:-resolve : ∀ {R S T} → T <: resolve (S ⇒ T) R
 <:-resolve {R} {S} {T} = <:-trans (<:-normalize T) (<:-resolveⁿ (normal (S ⇒ T)) (normal R))
 
-resolveˢ-<:-⇒ : ∀ {F R U} → (FunType F) → (Saturated F) → (r : Resolved F R) → (R ≮: never) → (F <: (R ⇒ U)) → (target r <: U)
-resolveˢ-<:-⇒ Fᶠ Fˢ r R≮:never F<:R⇒U with <:-impl-<:ᵒ Fᶠ Fˢ R≮:never F<:R⇒U
-resolveˢ-<:-⇒ Fᶠ Fˢ (yes Sʳ Tʳ oʳ R<:Sʳ tgtʳ) R≮:never F<:R⇒U | defn o o₁ o₂ = <:-trans (tgtʳ o o₁) o₂
-resolveˢ-<:-⇒ Fᶠ Fˢ (no tgtʳ) R≮:never F<:R⇒U | defn o o₁ o₂ = CONTRADICTION (<:-impl-¬≮: o₁ (tgtʳ o))
+resolveˢ-<:-⇒ : ∀ {F R U} → (FunType F) → (Saturated F) → (r : Resolved F R) → (F <: (R ⇒ U)) → (target r <: U)
+resolveˢ-<:-⇒ Fᶠ Fˢ r F<:R⇒U with <:-impl-<:ᵒ Fᶠ Fˢ F<:R⇒U
+resolveˢ-<:-⇒ Fᶠ Fˢ (yes Sʳ Tʳ oʳ R<:Sʳ tgtʳ) F<:R⇒U | defn o o₁ o₂ = <:-trans (tgtʳ o o₁) o₂
+resolveˢ-<:-⇒ Fᶠ Fˢ (no tgtʳ) F<:R⇒U | defn o o₁ o₂ = CONTRADICTION (<:-impl-¬≮: o₁ (tgtʳ o))
 
-resolveⁿ-<:-⇒ : ∀ {F R U} → (Fⁿ : Normal F) → (Rⁿ : Normal R) → (R ≮: never) → (F <: (R ⇒ U)) → (resolveⁿ Fⁿ Rⁿ <: U)
-resolveⁿ-<:-⇒ (Sⁿ ⇒ Tⁿ) Rⁿ R≮:never F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) (resolveˢ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) Rⁿ (λ o → o)) R≮:never F<:R⇒U
-resolveⁿ-<:-⇒ (Fⁿ ∩ Gⁿ) Rⁿ R≮:never F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) (resolveˢ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) Rⁿ (λ o → o)) R≮:never (<:-trans (saturate-<: (Fⁿ ∩ Gⁿ)) F<:R⇒U)
-resolveⁿ-<:-⇒ (Sⁿ ∪ Tˢ) Rⁿ R≮:never F<:R⇒U = CONTRADICTION (<:-impl-¬≮: F<:R⇒U (<:-trans-≮: <:-∪-right (scalar-≮:-function Tˢ)))
-resolveⁿ-<:-⇒ never Rⁿ R≮:never F<:R⇒U = <:-never
-resolveⁿ-<:-⇒ unknown Rⁿ R≮:never F<:R⇒U = CONTRADICTION (<:-impl-¬≮: F<:R⇒U unknown-≮:-function)
+resolveⁿ-<:-⇒ : ∀ {F R U} → (Fⁿ : Normal F) → (Rⁿ : Normal R) → (F <: (R ⇒ U)) → (resolveⁿ Fⁿ Rⁿ <: U)
+resolveⁿ-<:-⇒ (Sⁿ ⇒ Tⁿ) Rⁿ F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) (resolveˢ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) Rⁿ (λ o → o)) F<:R⇒U
+resolveⁿ-<:-⇒ (Fⁿ ∩ Gⁿ) Rⁿ F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) (resolveˢ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) Rⁿ (λ o → o)) (<:-trans (saturate-<: (Fⁿ ∩ Gⁿ)) F<:R⇒U)
+resolveⁿ-<:-⇒ (Sⁿ ∪ Tˢ) Rⁿ F<:R⇒U = CONTRADICTION (<:-impl-¬≮: F<:R⇒U (<:-trans-≮: <:-∪-right (scalar-≮:-function Tˢ)))
+resolveⁿ-<:-⇒ never Rⁿ F<:R⇒U = <:-never
+resolveⁿ-<:-⇒ unknown Rⁿ F<:R⇒U = CONTRADICTION (<:-impl-¬≮: F<:R⇒U unknown-≮:-function)
 
-resolve-<:-⇒ : ∀ {F R U} → (R ≮: never) → (F <: (R ⇒ U)) → (resolve F R <: U)
-resolve-<:-⇒ {F} {R} R≮:never F<:R⇒U = resolveⁿ-<:-⇒ (normal F) (normal R) (<:-trans-≮: (<:-normalize R) R≮:never) (<:-trans (normalize-<: F) (<:-trans F<:R⇒U (<:-function (normalize-<: R) <:-refl)))
+resolve-<:-⇒ : ∀ {F R U} → (F <: (R ⇒ U)) → (resolve F R <: U)
+resolve-<:-⇒ {F} {R} F<:R⇒U = resolveⁿ-<:-⇒ (normal F) (normal R) (<:-trans (normalize-<: F) (<:-trans F<:R⇒U (<:-function (normalize-<: R) <:-refl)))
 
-resolve-≮:-⇒ : ∀ {F R U} → (R ≮: never) → (resolve F R ≮: U) → (F ≮: (R ⇒ U))
-resolve-≮:-⇒ {F} {R} {U} R≮:never FR≮:U with dec-subtyping F (R ⇒ U)
-resolve-≮:-⇒ {F} {R} {U} R≮:never FR≮:U | Left F≮:R⇒U = F≮:R⇒U
-resolve-≮:-⇒ {F} {R} {U} R≮:never FR≮:U | Right F<:R⇒U = CONTRADICTION (<:-impl-¬≮: (resolve-<:-⇒ R≮:never F<:R⇒U) FR≮:U)
+resolve-≮:-⇒ : ∀ {F R U} → (resolve F R ≮: U) → (F ≮: (R ⇒ U))
+resolve-≮:-⇒ {F} {R} {U} FR≮:U with dec-subtyping F (R ⇒ U)
+resolve-≮:-⇒ {F} {R} {U} FR≮:U | Left F≮:R⇒U = F≮:R⇒U
+resolve-≮:-⇒ {F} {R} {U} FR≮:U | Right F<:R⇒U = CONTRADICTION (<:-impl-¬≮: (resolve-<:-⇒ F<:R⇒U) FR≮:U)
diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda
index 65d93049..c95a4f16 100644
--- a/prototyping/Properties/StrictMode.agda
+++ b/prototyping/Properties/StrictMode.agda
@@ -86,7 +86,7 @@ heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮:
 heap-weakeningᴱ Γ H (val (number x)) h p = p
 heap-weakeningᴱ Γ H (val (bool x)) h p = p
 heap-weakeningᴱ Γ H (val (string x)) h p = p
-heap-weakeningᴱ Γ H (M $ N) h p = ⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ Γ H N h (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ Γ H M h (resolve-≮:-⇒ {!!} p)))))
+heap-weakeningᴱ Γ H (M $ N) h p = ⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ Γ H N h (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ Γ H M h (resolve-≮:-⇒ p)))))
 heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p
 heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p
 heap-weakeningᴱ Γ H (binexp M op N) h p = p
@@ -107,7 +107,7 @@ substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ
 substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p
 substitutivityᴱ H (val w) v x p = Left p
 substitutivityᴱ H (binexp M op N) v x p = Left p
-substitutivityᴱ H (M $ N) v x p with substitutivityᴱ H M v x (resolve-≮:-⇒ {!!} p) 
+substitutivityᴱ H (M $ N) v x p with substitutivityᴱ H M v x (resolve-≮:-⇒ p) 
 substitutivityᴱ H (M $ N) v x p | Left q with substitutivityᴱ H N v x (⇒-≮:-resolve⁻¹ q)
 substitutivityᴱ H (M $ N) v x p | Left q | Left r = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ r))
 substitutivityᴱ H (M $ N) v x p | Left q | Right r = Right r
@@ -142,10 +142,10 @@ binOpPreservation H (·· v w) = refl
 reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M))
 reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B))
 
-reflect-subtypingᴱ H (M $ N) (app₁ s) p with reflect-subtypingᴱ H M s (resolve-≮:-⇒ {!!} p)
+reflect-subtypingᴱ H (M $ N) (app₁ s) p with reflect-subtypingᴱ H M s (resolve-≮:-⇒ p)
 reflect-subtypingᴱ H (M $ N) (app₁ s) p | Left q = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) (⇒-≮:-resolve⁻¹ q))))
 reflect-subtypingᴱ H (M $ N) (app₁ s) p | Right W = Right (app₁ W)
-reflect-subtypingᴱ H (M $ N) (app₂ v s) p with reflect-subtypingᴱ H N s (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (resolve-≮:-⇒ {!!} p)))
+reflect-subtypingᴱ H (M $ N) (app₂ v s) p with reflect-subtypingᴱ H N s (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (resolve-≮:-⇒ p)))
 reflect-subtypingᴱ H (M $ N) (app₂ v s) p | Left q = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ q))
 reflect-subtypingᴱ H (M $ N) (app₂ v s) p | Right W = Right (app₂ W)
 reflect-subtypingᴱ H (M $ N) {T = T} (beta (function f ⟨ var y ∈ S ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong (λ F → resolve F (typeOfᴱ H ∅ N)) (cong orUnknown (cong typeOfᴹᴼ q))) (<:-trans-≮: (<:-resolve {typeOfᴱ H ∅ N} {S} {U}) p))
diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda
index c9400d2e..eb78b8db 100644
--- a/prototyping/Properties/Subtyping.agda
+++ b/prototyping/Properties/Subtyping.agda
@@ -5,7 +5,7 @@ module Properties.Subtyping where
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
-open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
 open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
 open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
 open import Properties.Equality using (_≢_)
@@ -50,6 +50,11 @@ dec-language never t = Left never
 dec-language unknown t = Right unknown
 dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
 dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)
+dec-language nil (function-tgt t) = Left (scalar-function-tgt nil)
+dec-language (T₁ ⇒ T₂) (function-tgt t) = mapLR function-tgt function-tgt (dec-language T₂ t)
+dec-language boolean (function-tgt t) = Left (scalar-function-tgt boolean)
+dec-language number (function-tgt t) = Left (scalar-function-tgt number)
+dec-language string (function-tgt t) = Left (scalar-function-tgt string)
 
 -- ¬Language T is the complement of Language T
 language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
@@ -64,7 +69,9 @@ language-comp function (scalar-function ()) function
 language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₁ p)
 language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₁ q) = language-comp s q p₁
 language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₂ q) = language-comp t p₂ q
-language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
+language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p 
+language-comp (function-tgt t) (scalar-function-tgt ()) (function-tgt q)
+language-comp (function-tgt t) (function-tgt p) (function-tgt q) = language-comp t p q
 
 -- ≮: is the complement of <:
 ¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
@@ -221,6 +228,7 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function p q (function-ok s t) (function-ok₁ r) = function-ok₁ (<:-impl-⊇ p s r)
 <:-function p q (function-ok s t) (function-ok₂ r) = function-ok₂ (q t r)
 <:-function p q (function-err s) (function-err r) = function-err (<:-impl-⊇ p s r)
+<:-function p q (function-tgt t) (function-tgt r) = function-tgt (q t r)
 
 <:-function-∩-∩ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∩ S) ⇒ (T ∩ U))
 <:-function-∩-∩ function (function , function) = function
@@ -228,6 +236,7 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₁ q) = function-ok₁ (right q)
 <:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₂ q) = function-ok₂ (p , q)
 <:-function-∩-∩ (function-err s) (function-err p , q) = function-err (left p)
+<:-function-∩-∩ (function-tgt s) (function-tgt p , function-tgt q) = function-tgt (p , q)
 
 <:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U))
 <:-function-∩-∪ function (function , function) = function
@@ -235,6 +244,7 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function-∩-∪ (function-ok s t) (p₁ , function-ok₂ p₂) = function-ok₂ (right p₂)
 <:-function-∩-∪ (function-ok s t) (function-ok₂ p₁ , p₂) = function-ok₂ (left p₁)
 <:-function-∩-∪ (function-err s) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
+<:-function-∩-∪ (function-tgt t) (function-tgt p , q) = function-tgt (left p)
 
 <:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U))
 <:-function-∩ function (function , function) = function
@@ -242,6 +252,7 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function-∩ (function-ok s t) (function-ok₁ p₁ , p₂) = function-ok₁ p₁
 <:-function-∩ (function-ok s t) (function-ok₂ p₁ , function-ok₂ p₂) = function-ok₂ (p₁ , p₂)
 <:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂
+<:-function-∩ (function-tgt t) (function-tgt p₁ , function-tgt p₂) = function-tgt (p₁ , p₂)
 
 <:-function-∪ : ∀ {R S T U} → ((R ⇒ S) ∪ (T ⇒ U)) <: ((R ∩ T) ⇒ (S ∪ U))
 <:-function-∪ function (left function) = function
@@ -254,6 +265,8 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function-∪ (function-ok s t) (right (function-ok₂ p)) = function-ok₂ (right p)
 <:-function-∪ (function-err s) (right (function-err x)) = function-err (right x)
 <:-function-∪ (scalar s) (right (scalar ()))
+<:-function-∪ (function-tgt t) (left (function-tgt p)) = function-tgt (left p)
+<:-function-∪ (function-tgt t) (right (function-tgt p)) = function-tgt (right p)
 
 <:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U))
 <:-function-∪-∩ function function = left function
@@ -263,12 +276,8 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function-∪-∩ (function-ok s t) (function-ok₂ (right p)) = right (function-ok₂ p)
 <:-function-∪-∩ (function-err s) (function-err (left p)) = left (function-err p)
 <:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p)
-
-<:-function-never : ∀ {T U} → (never ⇒ T) <: (never ⇒ U)
-<:-function-never function function = function
-<:-function-never (function-ok s t) (function-ok₁ p) = function-ok₁ p
-<:-function-never (function-ok s t) (function-ok₂ p) = function-ok₁ never
-<:-function-never (function-err s) (function-err p) = function-err p
+<:-function-∪-∩ (function-tgt t) (function-tgt (left p)) = left (function-tgt p)
+<:-function-∪-∩ (function-tgt t) (function-tgt (right p)) = right (function-tgt p)
 
 <:-function-left : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R <: S)
 <:-function-left {R} {S} p s Rs with dec-language S s
@@ -364,6 +373,7 @@ function-≮:-never = witness function function never
 <:-everything function p = left function
 <:-everything (function-ok s t) p = left (function-ok₁ never)
 <:-everything (function-err s) p = left (function-err never)
+<:-everything (function-tgt t) p = left (function-tgt unknown)
 
 -- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
 -- defines a "set-theoretic" model (sec 2.5)
@@ -415,23 +425,28 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _)
   S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
   S₁t | Right r = r
 
-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
+not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
+
+  -- We don't quite have that this is a set-theoretic model
+  -- it's only true when Language S₂ is inhabited
+  -- in particular it's not true when S₂ is never,
+  ∀ s₂ → Language S₂ s₂ →
 
   -- This is the "only if" part of being a set-theoretic model
-  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂)))) →
+  (∀ Q → Q ⊆ Comp(Language S₁ ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp(Language S₂ ⊗ Comp(Lift(Language T₂)))) →
   (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂))
 
-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} p = r where
+not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ S₂s₂ p = r where
 
   Q : (Tree × Maybe Tree) → Set
   Q (t , just u) = Either (¬Language S₁ t) (Language T₁ u)
   Q (t , nothing) = ¬Language S₁ t
-
-  q : Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁)))
+  
+  q : Q ⊆ Comp(Language S₁ ⊗ Comp(Lift(Language T₁)))
   q (t , just u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
   q (t , just u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u
   q (t , nothing) ¬S₁t (S₁t , _) = language-comp t ¬S₁t S₁t
-
+  
   r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)
   r function function = function
   r (function-err s) (function-err ¬S₁s) with dec-language S₂ s
@@ -445,3 +460,14 @@ set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} p = r where
   r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Left ¬S₂s = function-ok₁ ¬S₂s
   r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Right S₂s = CONTRADICTION (p Q q (s , just t) (Right T₁t) (S₂s , language-comp t ¬T₂t))
   r (function-ok s t) (function-ok₂ T₁t) | Right T₂t = function-ok₂ T₂t
+  r (function-tgt t) (function-tgt T₁t) with dec-language T₂ t
+  r (function-tgt t) (function-tgt T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
+  r (function-tgt t) (function-tgt T₁t) | Right T₂t = function-tgt T₂t
+
+-- A counterexample when the argument type is empty.
+
+set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Language number)) → Q ⊆ Comp((Language never) ⊗ Comp(Language string)))
+set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)
+
+set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string)
+set-theoretic-counterexample-two = witness (function-tgt (scalar number)) (function-tgt (scalar number)) (function-tgt (scalar-scalar number string (λ ())))
diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda
index a2977dfd..49f6df22 100644
--- a/prototyping/Properties/TypeNormalization.agda
+++ b/prototyping/Properties/TypeNormalization.agda
@@ -6,7 +6,7 @@ open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never;
 open import Luau.Subtyping using (Tree; Language; function; scalar; unknown; right; scalar-function-err; _,_)
 open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize)
 open import Luau.Subtyping using (_<:_; _≮:_; witness; never)
-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)
+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)
 
 -- Normal forms for types
 data FunType : Type → Set
diff --git a/prototyping/Properties/TypeSaturation.agda b/prototyping/Properties/TypeSaturation.agda
index b2e35473..b5bc068c 100644
--- a/prototyping/Properties/TypeSaturation.agda
+++ b/prototyping/Properties/TypeSaturation.agda
@@ -8,7 +8,7 @@ open import Luau.Subtyping using (Tree; Language; ¬Language; _<:_; _≮:_; witn
 open import Luau.Type using (Type; _⇒_; _∩_; _∪_; never; unknown)
 open import Luau.TypeNormalization using (_∩ⁿ_; _∪ⁿ_)
 open import Luau.TypeSaturation using (_⋓_; _⋒_; _∩ᵘ_; _∩ⁱ_; ∪-saturate; ∩-saturate; saturate)
-open import Properties.Subtyping using (dec-language; language-comp; <:-impl-⊇; <:-refl; <:-trans; <:-trans-≮:; <:-impl-¬≮: ; <:-never; <:-unknown; <:-function; <:-union; <:-∪-symm; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∪-assocl; <:-∪-assocr; <:-intersect; <:-∩-symm; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-function-left; ≮:-function-right; <:-function-never; <:-function-∩-∪; <:-function-∩-∩; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
+open import Properties.Subtyping using (dec-language; language-comp; <:-impl-⊇; <:-refl; <:-trans; <:-trans-≮:; <:-impl-¬≮: ; <:-never; <:-unknown; <:-function; <:-union; <:-∪-symm; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∪-assocl; <:-∪-assocr; <:-intersect; <:-∩-symm; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-function-left; ≮:-function-right; <:-function-∩-∪; <:-function-∩-∩; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
 open import Properties.TypeNormalization using (Normal; FunType; _⇒_; _∩_; _∪_; never; unknown; function-top; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
 open import Properties.Contradiction using (CONTRADICTION)
 open import Properties.Functions using (_∘_)