diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda
index decdc113..4c5a81d6 100644
--- a/prototyping/Properties/DecSubtyping.agda
+++ b/prototyping/Properties/DecSubtyping.agda
@@ -10,10 +10,37 @@ open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never;
 open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
 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-∩; <:-union; ≮:-left-∪; ≮:-right-∪; <:-impl-⊇)
-open import Properties.TypeNormalization using (FunType; Normal; never; unknown; function; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; normalⁱ)
+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; function; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalⁱ; normalᶠ)
 open import Properties.Equality using (_≢_)
 
+fun-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
+fun-top function = <:-refl
+fun-top (S ⇒ T) = <:-function <:-never <:-unknown
+fun-top (F ∩ G) = <:-trans <:-∩-left (fun-top F)
+
+fun-function : ∀ {F} → FunType F → Language F function
+fun-function function = function
+fun-function (S ⇒ T) = function
+fun-function (F ∩ G) = (fun-function F , fun-function G)
+
+¬fun-scalar : ∀ {F S} → (s : Scalar S) → FunType F → ¬Language F (scalar s)
+¬fun-scalar = {!!}
+
+fun-¬scalar : ∀ {F S t} → (s : Scalar S) → FunType F → Language F t → ¬Language S t
+fun-¬scalar s function function = scalar-function s
+fun-¬scalar s function (function-ok₁ p) = scalar-function-ok s
+fun-¬scalar s function (function-ok₂ p) = scalar-function-ok s
+fun-¬scalar s function (function-err p) = scalar-function-err s
+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 (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂
+
+function-err-ok : ∀ {F s t} → FunType F → Language F (function-err s) → Language F (function-ok s t)
+function-err-ok = {!!}
+
 -- Honest this terminates, since src and tgt reduce the depth of nested arrows
 {-# TERMINATING #-}
 dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
@@ -29,12 +56,9 @@ srcᶠ-function-err : ∀ {F} → (Fᶠ : FunType F) → ∀ s → ¬Language (s
 
 resolveᶠⁿ : ∀ {F V} → FunType F → Normal V → Type
 normal-resolveᶠⁿ : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → Normal (resolveᶠⁿ Fᶠ Vⁿ)
-resolveᶠⁿ-function-ok : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → (V <: srcᶠ Fᶠ) → ∀ s t → Language (srcᶠ Fᶠ) s → ¬Language (resolveᶠⁿ Fᶠ Vⁿ) t → ¬Language F (function-ok s t)
-≮:-resolveᶠⁿ : ∀ {F S T} → (Fᶠ : FunType F) → (Sᶠ : Normal S) → (S <: srcᶠ Fᶠ) → (resolveᶠⁿ Fᶠ Sᶠ ≮: T) → (F ≮: (S ⇒ T))
-<:-resolveᶠⁿ : ∀ {F S T} → (Fᶠ : FunType F) → (Sᶠ : Normal S) → (S <: srcᶠ Fᶠ) → (resolveᶠⁿ Fᶠ Sᶠ <: T) → (F <: (S ⇒ T))
-
-fun-function : ∀ {F} → FunType F → Language F function
-¬fun-scalar : ∀ {F S} → (s : Scalar S) → FunType F → ¬Language F (scalar s)
+-- function-ok-resolveᶠⁿ : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → (V <: srcᶠ Fᶠ) → ∀ s t → Language V s → Language F (function-ok s t) → Language (resolveᶠⁿ Fᶠ Vⁿ) t
+≮:-resolveᶠⁿ : ∀ {F S T} → (Fᶠ : FunType F) → (Sᶠ : Normal S) → (S <: srcᶠ Fᶠ) → (S ≮: never) → (resolveᶠⁿ Fᶠ Sᶠ ≮: T) → (F ≮: (S ⇒ T))
+<:-resolveᶠⁿ : ∀ {F S} → (Fᶠ : FunType F) → (Sⁿ : Normal S) → (S <: srcᶠ Fᶠ) → (F <: (S ⇒ resolveᶠⁿ Fᶠ Sⁿ))
 
 srcᶠ {S ⇒ T} F = S
 srcᶠ (F ∩ G) = srcᶠ F ∪ⁿ srcᶠ G
@@ -52,7 +76,7 @@ srcᶠ-function-err (F ∩ G) s p | (p₁ , p₂) = (srcᶠ-function-err F s p
 
 resolveᶠⁿ {S ⇒ T} F V = T
 resolveᶠⁿ (F ∩ G) V with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
-resolveᶠⁿ (F ∩ G) V | Left p | Left q = resolveᶠⁿ F V ∪ⁿ resolveᶠⁿ G V
+resolveᶠⁿ (F ∩ G) V | Left p | Left q = resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V) ∪ⁿ resolveᶠⁿ G (normal-∩ⁿ (normal-srcᶠ G) V)
 resolveᶠⁿ (F ∩ G) V | Left p | Right q = resolveᶠⁿ G V
 resolveᶠⁿ (F ∩ G) V | Right p | Left q = resolveᶠⁿ F V
 resolveᶠⁿ (F ∩ G) V | Right p | Right q = resolveᶠⁿ F V ∩ⁿ resolveᶠⁿ G V
@@ -60,35 +84,54 @@ resolveᶠⁿ (F ∩ G) V | Right p | Right q = resolveᶠⁿ F V ∩ⁿ resolve
 normal-resolveᶠⁿ function V = unknown
 normal-resolveᶠⁿ (S ⇒ T) V = T
 normal-resolveᶠⁿ (F ∩ G) V with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
-normal-resolveᶠⁿ (F ∩ G) V | Left p | Left q = normal-∪ⁿ (normal-resolveᶠⁿ F V) (normal-resolveᶠⁿ G V)
+normal-resolveᶠⁿ (F ∩ G) V | Left p | Left q = normal-∪ⁿ (normal-resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V)) (normal-resolveᶠⁿ G (normal-∩ⁿ (normal-srcᶠ G) V))
 normal-resolveᶠⁿ (F ∩ G) V | Left p | Right q = normal-resolveᶠⁿ G V
 normal-resolveᶠⁿ (F ∩ G) V | Right p | Left q = normal-resolveᶠⁿ F V
 normal-resolveᶠⁿ (F ∩ G) V | Right p | Right q = normal-∩ⁿ (normal-resolveᶠⁿ F V) (normal-resolveᶠⁿ G V)
 
-resolveᶠⁿ-function-ok function V p₀ s t (scalar ()) q
-resolveᶠⁿ-function-ok (S ⇒ T) V p₀ s t p₁ p₂ = function-ok p₁ p₂
-resolveᶠⁿ-function-ok (F ∩ G) V p₀ s t p₁ p₂ with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G) | ∪ⁿ-<:-∪ (normal-srcᶠ F) (normal-srcᶠ G) s p₁
-resolveᶠⁿ-function-ok (F ∩ G) V p₀ s t p₁ p₂ | Left q₁ | Left q₂ | q₃ with <:-impl-⊇ (∪-<:-∪ⁿ (normal-resolveᶠⁿ F V) (normal-resolveᶠⁿ G V)) t p₂
-resolveᶠⁿ-function-ok (F ∩ G) V p₀ s t p₁ p₂ | Left q₁ | Left q₂ | left q₃ | (r₁ , r₂) = left (resolveᶠⁿ-function-ok F V {!p₀!} s t q₃ r₁)
-resolveᶠⁿ-function-ok (F ∩ G) V p₀ s t p₁ p₂ | Left q₁ | Left q₂ | right q₃ | (r₁ , r₂) = right (resolveᶠⁿ-function-ok G V {!!} s t q₃ r₂)
-resolveᶠⁿ-function-ok (F ∩ G) V p₀ s t p₁ p₂ | Left q₁ | Right q₂ | q₃ = {!resolveᶠⁿ-function-ok G V s t!}
+-- function-ok-resolveᶠⁿ function V p s t q₁ q₂ = {!!}
+-- function-ok-resolveᶠⁿ (S ⇒ T) V p s t q₁ q₂ = {!!}
+-- function-ok-resolveᶠⁿ (F ∩ G) V p s t q₁ (q₂ , q₃) with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
+-- function-ok-resolveᶠⁿ (F ∩ G) V p s t q₁ (q₂ , q₃) | Left r₁ | Left r₂ with ∪ⁿ-<:-∪ (normal-srcᶠ F) (normal-srcᶠ G) s (p s q₁)
+-- function-ok-resolveᶠⁿ (F ∩ G) V p s t q₁ (q₂ , q₃) | Left r₁ | Left r₂ | left r₃ = ∪-<:-∪ⁿ (normal-resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V))
+--                                                                                      (normal-resolveᶠⁿ G (normal-∩ⁿ (normal-srcᶠ G) V)) t (left {!function-ok-resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V) ? s t ? !}) -- ∪-<:-∪ⁿ (normal-resolveᶠⁿ F V) {!normal-resolveᶠⁿ G V!} t (left (function-ok-resolveᶠⁿ F V {!!} s t q₁ q₂))
 
-≮:-resolveᶠⁿ F S p (witness t q r) = witness {!function-ok !} {!!} {!p!}
 
-<:-resolveᶠⁿ F S p q = {!!}
+<:-resolveᶠⁿ function V p = <:-function p <:-refl
+<:-resolveᶠⁿ (S ⇒ T) V p = <:-function p <:-refl
+<:-resolveᶠⁿ (F ∩ G) V p with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
+<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Left q | Left r = result where
 
-fun-function F = {!!}
-¬fun-scalar s F = {!!}
+  T = resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ)
+  U = resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ)
+  
+  Tⁿ = normal-resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ)
+  Uⁿ = normal-resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ)
+  
+  lemma₁ : F <: ((srcᶠ Fᶠ ∩ V) ⇒ T)
+  lemma₁ = <:-trans (<:-resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ) (<:-trans (∩ⁿ-<:-∩ (normal-srcᶠ Fᶠ) Vⁿ) <:-∩-left)) (<:-function (∩-<:-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ) <:-refl)
+
+  lemma₂ : G <: ((srcᶠ Gᶠ ∩ V) ⇒ U)
+  lemma₂ = <:-trans (<:-resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ) (<:-trans (∩ⁿ-<:-∩ (normal-srcᶠ Gᶠ) Vⁿ) <:-∩-left)) (<:-function (∩-<:-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ) <:-refl)
+
+  result : (F ∩ G) <: (V ⇒ (T ∪ⁿ U))
+  result = <:-trans (<:-trans (<:-intersect lemma₁ lemma₂) <:-function-∩-∪) (<:-function (<:-trans (<:-∩-glb (<:-trans p (∪ⁿ-<:-∪ (normal-srcᶠ Fᶠ) (normal-srcᶠ Gᶠ))) <:-refl) <:-∩-distr-∪) (∪-<:-∪ⁿ Tⁿ Uⁿ))
+
+<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Left q | Right r = <:-trans <:-∩-right (<:-resolveᶠⁿ Gᶠ Vⁿ r)
+<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Right q | Left r = <:-trans <:-∩-left (<:-resolveᶠⁿ Fᶠ Vⁿ q)
+<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Right q | Right r = <:-trans (<:-intersect (<:-resolveᶠⁿ Fᶠ Vⁿ q) (<:-resolveᶠⁿ Gᶠ Vⁿ r)) (<:-trans <:-function-∩ (<:-function <:-refl (∩-<:-∩ⁿ (normal-resolveᶠⁿ Fᶠ Vⁿ) (normal-resolveᶠⁿ Gᶠ Vⁿ))))
+
+≮:-resolveᶠⁿ F V p (witness s q₁ q₂) (witness t r₁ r₂) = witness (function-ok s t) {!!} (function-ok q₁ {!r₂!})
 
 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ᶠ T function = Right (fun-top T)
 dec-subtypingᶠ T (U ⇒ V) with dec-subtypingⁿ (normalⁱ U) (normal-srcᶠ T) | dec-subtypingⁿ (normal-resolveᶠⁿ T (normalⁱ U)) V
 dec-subtypingᶠ T (U ⇒ V) | Left p | q = Left (≮:-srcᶠ T p)
-dec-subtypingᶠ T (U ⇒ V) | Right p | Left q = Left (≮:-resolveᶠⁿ T (normalⁱ U) p q)
-dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (<:-resolveᶠⁿ T (normalⁱ U) p q)
-
+dec-subtypingᶠ T (U ⇒ V) | Right p | Left q = Left {!q!} -- Left (<:-trans-≮: {!!} (≮:-function-right {!!} q)) -- (≮:-resolveᶠⁿ T (normalⁱ U) p q)
+dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (<:-trans (<:-resolveᶠⁿ T (normalⁱ U) p) (<:-function <:-refl q))
 dec-subtypingᶠ T (U ∩ V) with dec-subtypingᶠ T U | dec-subtypingᶠ T V
 dec-subtypingᶠ T (U ∩ V) | Left p | q = Left (≮:-∩-left p)
 dec-subtypingᶠ T (U ∩ V) | Right p | Left q = Left (≮:-∩-right q)
@@ -96,10 +139,11 @@ dec-subtypingᶠ T (U ∩ V) | Right p | Right q = Right (<:-∩-glb p q)
 
 dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
 dec-subtypingᶠⁿ T unknown = Right <:-unknown
+dec-subtypingᶠⁿ T function = Right (fun-top T)
 dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V)
 dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V)
 dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U
-dec-subtypingᶠⁿ T (U ∪ V) | Left (witness t p q) = Left (witness t p (q , {!!}))
+dec-subtypingᶠⁿ T (U ∪ V) | Left (witness t p q) = Left (witness t p (q , fun-¬scalar V T p))
 dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)
 
 dec-subtypingⁿ never U = Right <:-never
@@ -122,9 +166,9 @@ dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p)
 dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q)
 dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q)
 dec-subtypingⁿ function function = Right <:-refl
-dec-subtypingⁿ function (T ⇒ U) = {!!}
-dec-subtypingⁿ function (T ∩ U) = {!!}
-dec-subtypingⁿ function (T ∪ U) = {!!}
+dec-subtypingⁿ function (T ⇒ U) = dec-subtypingᶠ function (T ⇒ U)
+dec-subtypingⁿ function (T ∩ U) = dec-subtypingᶠ function (T ∩ U)
+dec-subtypingⁿ function (T ∪ U) = dec-subtypingᶠⁿ function (T ∪ U)
 dec-subtypingⁿ function never = Left (witness function function never)
 dec-subtypingⁿ function unknown = Right <:-unknown