diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean
new file mode 100644
index 00000000..b19f479b
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean
@@ -0,0 +1,49 @@
+/-
+# Type soundness of System F<:
+
+This mechanizes type soundness for System F<: using intrinsically scoped de Bruijn indices
+and context morphisms.
+
+The formalization uses intrinsically scoped de Bruijn indices.
+De Bruijn indices are indexed by signatures describing available binders in the type context.
+Syntactic constructs are well-scoped by construction.
+
+Context morphisms are mappings between type contexts that preserve types.
+All theorems concerning context operations (weakening, narrowing, substitution)
+are proven uniformly using these morphisms.
+
+Two kinds of context morphisms exist:
+
+Rebinding morphisms map each `x:T ∈ Γ` to a corresponding binder `f(x) : f(T) ∈ Δ`.
+Typing is preserved under rebinding morphisms.
+
+Retyping morphisms map each `x: T ∈ Γ` to a typing derivation `Δ ⊢ g(x) : g(T)`.
+This is stronger than rebinding morphisms.
+The proof builds on rebinding morphism preservation.
+
+This infrastructure enables proofs for context manipulation operations including
+weakening, narrowing, substitution, and any context operations expressible as context morphisms.
+-/
+
+-- This module defines the intrinsically scoped de Bruijn indices.
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Debruijn
+
+-- The following modules define Syetem F<:.
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Eval
+
+-- The following defines parallel substitution and proves its properties.
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties
+
+-- The following modules define context morphisms and prove their theory.
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem
+
+-- Main type soundness results.
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Preservation
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Progress
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean
new file mode 100644
index 00000000..88c1ddd3
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean
@@ -0,0 +1,169 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Intrinsically scoped de Bruijn indices
+
+This module defines the foundation for intrinsically scoped de Bruijn indices used throughout
+the System F<: mechanization.
+Instead of using raw natural numbers for de Bruijn indices,
+variables and type variables are indexed by a signature (`Sig`) that describes
+the available binders in the context.
+
+This approach ensures that syntactic constructs are well-scoped by construction,
+eliminating the possibility of free variables and making theorems easier to state and prove.
+
+The module defines:
+- `Sig`: Signatures that describe the structure of typing contexts
+- `Var` and `TVar`: Intrinsically scoped variables and type variables
+- `Rename`: Renamings between different signatures
+- Context lifting operations for working under binders
+-/
+
+import Mathlib.Tactic
+
+/-- A signature describes the structure of a typing context, tracking both
+    term variables and type variables in the order they were introduced. -/
+inductive Sig : Type where
+| empty : Sig
+/-- Extend signature with a term variable -/
+| push_var : Sig → Sig
+/-- Extend signature with a type variable -/
+| push_tvar : Sig → Sig
+
+@[simp]
+instance : EmptyCollection Sig := ⟨Sig.empty⟩
+
+theorem Sig.empty_eq : {} = Sig.empty := rfl
+
+/-- Convenient syntax for extending a signature with a term variable -/
+postfix:50 ",x" => Sig.push_var
+/-- Convenient syntax for extending a signature with a type variable -/
+postfix:50 ",X" => Sig.push_tvar
+
+/-- Term variables indexed by signatures. A `Var s` represents a term variable
+    that is valid in signature `s`. The constructors correspond to different ways
+    a variable can be accessed from the current context. -/
+inductive Var : Sig → Type where
+/-- The most recently bound term variable -/
+| here : Var (s,x)
+/-- Skip over the most recent term variable -/
+| there_var : Var s → Var (s,x)
+/-- Skip over the most recent type variable -/
+| there_tvar : Var s → Var (s,X)
+
+/-- Type variables indexed by signatures. A `TVar s` represents a type variable
+    that is valid in signature `s`. -/
+inductive TVar : Sig → Type where
+/-- The most recently bound type variable -/
+| here : TVar (s,X)
+/-- Skip over the most recent term variable -/
+| there_var : TVar s → TVar (s,x)
+/-- Skip over the most recent type variable -/
+| there_tvar : TVar s → TVar (s,X)
+
+/-- A renaming between signatures `s1` and `s2` specifies how to map variables
+    from `s1` to variables in `s2`. This is the foundation for all variable
+    renamings in the mechanization. -/
+structure Rename (s1 s2 : Sig) where
+  /-- How to rename term variables -/
+  var : Var s1 → Var s2
+  /-- How to rename type variables -/
+  tvar : TVar s1 → TVar s2
+
+/-- Lift a renaming to work under a new term variable binder. The new term variable
+    is mapped to itself, while existing variables are renamed and shifted. -/
+def Rename.liftVar (f : Rename s1 s2) : Rename (s1,x) (s2,x) where
+  var := fun x => match x with
+    | .here => .here
+    | .there_var x0 => .there_var (f.var x0)
+  tvar := fun X => match X with
+    | .there_var X0 => .there_var (f.tvar X0)
+
+/-- Lift a renaming to work under a new type variable binder. The new type variable
+    is mapped to itself, while existing variables are renamed and shifted. -/
+def Rename.liftTVar (f : Rename s1 s2) : Rename (s1,X) (s2,X) where
+  tvar := fun X => match X with
+    | .here => .here
+    | .there_tvar X0 => .there_tvar (f.tvar X0)
+  var := fun x => match x with
+    | .there_tvar x0 => .there_tvar (f.var x0)
+
+/-- Weakening renaming that adds a new term variable to the context.
+    All existing variables are shifted to account for the new binding. -/
+def Rename.succVar : Rename s1 (s1,x) where
+  var := fun x => x.there_var
+  tvar := fun X => X.there_var
+
+/-- Weakening renaming that adds a new type variable to the context.
+    All existing variables are shifted to account for the new binding. -/
+def Rename.succTVar : Rename s1 (s1,X) where
+  var := fun x => x.there_tvar
+  tvar := fun X => X.there_tvar
+
+/-- The identity renaming that maps each variable to itself. -/
+def Rename.id : Rename s s where
+  var := fun x => x
+  tvar := fun X => X
+
+/-- Composition of renamings. If `f1` renames from `s1` to `s2` and `f2` renames
+    from `s2` to `s3`, then their composition renames from `s1` to `s3`. -/
+def Rename.comp (f1 : Rename s1 s2) (f2 : Rename s2 s3) : Rename s1 s3 where
+  var := fun x => f2.var (f1.var x)
+  tvar := fun X => f2.tvar (f1.tvar X)
+
+/-- Two renamings are equal if they map variables in the same way. -/
+theorem Rename.funext {f g : Rename s1 s2}
+  (var : ∀ x, f.var x = g.var x)
+  (tvar : ∀ X, f.tvar X = g.tvar X) : f = g := by
+  cases f; cases g
+  aesop
+
+/-- Lifting the identity renaming gives the identity renaming. -/
+@[simp]
+theorem Rename.id_liftVar_eq_id : Rename.id.liftVar = (Rename.id (s:=(s,x))) := by
+  apply Rename.funext <;> intro x <;> cases x <;> rfl
+
+/-- Lifting the identity renaming gives the identity renaming. -/
+@[simp]
+theorem Rename.id_liftTVar_eq_id : Rename.id.liftTVar = (Rename.id (s:=(s,X))) := by
+  apply Rename.funext <;> intro X <;> cases X <;> rfl
+
+/-- Composition commutes with lifting over type variables. -/
+theorem Rename.comp_liftTVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} :
+  (f1.comp f2).liftTVar = f1.liftTVar.comp f2.liftTVar := by
+  apply Rename.funext <;> intro X <;> cases X <;> rfl
+
+/-- Composition commutes with lifting over term variables. -/
+theorem Rename.comp_liftVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} :
+  (f1.comp f2).liftVar = f1.liftVar.comp f2.liftVar := by
+  apply Rename.funext <;> intro x <;> cases x <;> rfl
+
+/-- Composing with variable weakening commutes with lifting. -/
+theorem Rename.rename_succVar_comm {f : Rename s1 s2} :
+  (f.comp Rename.succVar) = Rename.succVar.comp f.liftVar := by
+  apply Rename.funext <;> aesop
+
+/-- Composing with type variable weakening commutes with lifting. -/
+theorem Rename.rename_succTVar_comm {f : Rename s1 s2} :
+  (f.comp Rename.succTVar) = Rename.succTVar.comp f.liftTVar := by
+  apply Rename.funext <;> aesop
+
+/-- Append two signatures, concatenating their binder sequences. -/
+def Sig.append : Sig → Sig → Sig
+| s1, .empty => s1
+| s1, .push_var s2 => .push_var (s1.append s2)
+| s1, .push_tvar s2 => .push_tvar (s1.append s2)
+
+@[simp]
+instance : Append Sig := ⟨Sig.append⟩
+
+/-- Lift a renaming to work under multiple binders specified by a signature.
+    This is the generalization of `liftVar` and `liftTVar` to arbitrary sequences of binders. -/
+def Rename.lift : Rename s1 s2 → (s : Sig) → Rename (s1 ++ s) (s2 ++ s)
+| f, .empty => f
+| f, .push_var s => (f.lift s).liftVar
+| f, .push_tvar s => (f.lift s).liftTVar
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean
new file mode 100644
index 00000000..264b8742
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Big-step evaluator for System F<:
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax
+
+/-- The result of evaluating an expression. Evaluation may succeed with a value,
+    fail with an error, or exhaust its fuel allocation. -/
+inductive Result (s : Sig) where
+/-- Successful evaluation to a value -/
+| ok : Exp s → Result s
+/-- Runtime error (e.g., free variable, type mismatch) -/
+| err : Result s
+/-- Evaluation did not terminate within fuel limit -/
+| nonterm : Result s
+
+/-- Big-step evaluator with fuel-based termination. -/
+def eval : Nat → Exp s → Result s
+| 0, _ => .nonterm
+| _, .var _ => .err
+| _, .abs A e => .ok (.abs A e)
+| _, .tabs S e => .ok (.tabs S e)
+| fuel+1, .app e1 e2 =>
+  match eval fuel e1 with
+  | .ok (.abs _ t1) =>
+    eval fuel (t1.open_var e2)
+  | .ok _ => .err
+  | .err => .err
+  | .nonterm => .nonterm
+| fuel+1, .tapp e A =>
+  match eval fuel e with
+  | .ok (.tabs _ t) =>
+    eval fuel (t.open_tvar A)
+  | .ok _ => .err
+  | .err => .err
+  | .nonterm => .nonterm
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean
new file mode 100644
index 00000000..1b87b1b2
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean
@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Rebinding morphisms
+
+This module defines rebinding morphisms, which enable systematic reasoning about
+context transformations in the well-scoped approach to System F<:.
+Rebinding morphisms are structure-preserving maps between typing contexts
+that maintain relationships between variables and their types.
+
+A rebinding morphism `ρ : Rebind Γ f Δ` consists of:
+- A renaming `f : s₁ → s₂` between signatures
+- Contexts `Γ : Ctx s₁` and `Δ : Ctx s₂`
+- Proofs that bound types are preserved under renaming
+
+If `x : T ∈ Γ` then `f(x) : f(T) ∈ Δ`, where `f(T)` denotes the renaming of type `T` under `f`.
+
+Rebinding theory forms the first layer in a hierarchy of context morphisms.
+Retyping morphisms build upon this foundation.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax
+
+/-- A rebinding morphism `Rebind Γ f Δ` witnesses that contexts `Γ` and `Δ` are
+    related by the renaming `f` in a type-preserving way.
+
+    This structure encodes the fundamental principle that context transformations
+    must preserve the variable and type bindings in the context. -/
+structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where
+  /-- Term variable preservation: x:T in Γ implies f(x):f(T) in Δ -/
+  var : ∀ x T,
+    (hb : Ctx.LookupVar Γ x T) →
+    Ctx.LookupVar Δ (f.var x) (T.rename f)
+  /-- Type variable preservation: X<:T in Γ implies f(X)<:f(T) in Δ -/
+  tvar : ∀ X T,
+    (hb : Ctx.LookupTVar Γ X T) →
+    Ctx.LookupTVar Δ (f.tvar X) (T.rename f)
+
+/-- **Lifting rebinding morphisms over term variable binders**.
+
+    If ρ witnesses that Γ and Δ are related by f, then ρ.liftVar witnesses
+    that Γ,x:T and Δ,x:f(T) are related by f.liftVar. -/
+def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) where
+  var := fun x P hb => by
+    cases hb
+    case here => simp only [←Ty.rename_succVar_comm]; constructor
+    case there_var hb =>
+      simp only [←Ty.rename_succVar_comm]
+      constructor
+      apply ρ.var _ _ hb
+  tvar := fun X S hb => by
+    cases hb
+    case there_var hb =>
+      simp only [←Ty.rename_succVar_comm]
+      constructor
+      apply ρ.tvar _ _ hb
+
+/-- **Lifting rebinding morphisms over type variable binders**.
+
+    If ρ witnesses that Γ and Δ are related by f, then ρ.liftTVar witnesses
+    that Γ,X<:T and Δ,X<:f(T) are related by f.liftTVar. -/
+def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) where
+  tvar := fun X S hb => by
+    cases hb
+    case here => simp only [←Ty.rename_succTVar_comm]; constructor
+    case there_tvar hb =>
+      simp only [←Ty.rename_succTVar_comm]
+      constructor
+      apply ρ.tvar _ _ hb
+  var := fun x P hb => by
+    cases hb
+    case there_tvar hb => simp only [←Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb
+
+/-- **Term variable weakening morphism**.
+
+    The standard weakening operation that extends a context with a new term variable
+    is a rebinding morphism. -/
+def Rebind.succVar : Rebind Γ Rename.succVar (Γ,x:T) where
+  var := by intro x P hb; constructor; exact hb
+  tvar := by intro X S hb; constructor; exact hb
+
+/-- **Type variable weakening morphism**.
+
+    The standard weakening operation that extends a context with a new type variable
+    is a rebinding morphism. -/
+def Rebind.succTVar : Rebind Γ Rename.succTVar (Γ,X<:T) where
+  tvar := by intro X S hb; constructor; exact hb
+  var := by intro x P hb; constructor; exact hb
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean
new file mode 100644
index 00000000..cd317a68
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties
+
+theorem Subtyp.rebind {f : Rename s1 s2}
+  (hs : Subtyp Γ T1 T2)
+  (ρ : Rebind Γ f Δ) :
+  Subtyp Δ (T1.rename f) (T2.rename f) := by
+  induction hs generalizing s2 <;> try (solve | constructor)
+  case trans => apply Subtyp.trans <;> aesop
+  case tvar hb =>
+    apply Subtyp.tvar
+    apply ρ.tvar _ _ hb
+  case arrow ih1 ih2 =>
+    apply Subtyp.arrow <;> grind
+  case poly ih1 ih2 =>
+    apply Subtyp.poly <;> try grind
+    · apply ih2 ρ.liftTVar
+
+theorem HasType.rebind {f : Rename s1 s2}
+  (ht : HasType Γ t T)
+  (ρ : Rebind Γ f Δ) :
+  HasType Δ (t.rename f) (T.rename f) := by
+  induction ht generalizing s2
+  case var hb =>
+    apply HasType.var
+    apply ρ.var _ _ hb
+  case sub hsub _ ih =>
+    apply sub
+    · apply hsub.rebind ρ
+    · apply ih ρ
+  case abs ih =>
+    apply HasType.abs
+    simp only [Ty.rename_succVar_comm]
+    apply ih ρ.liftVar
+  case tabs ih =>
+    apply HasType.tabs
+    apply ih ρ.liftTVar
+  case app ih1 ih2 =>
+    apply HasType.app
+    · apply ih1 ρ
+    · apply ih2 ρ
+  case tapp ih =>
+    simp only [Ty.open_tvar_rename_comm]
+    apply tapp
+    aesop
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean
new file mode 100644
index 00000000..e3ce35b1
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Operational semantics for System F<:
+
+This module defines the small-step operational semantics for System F<:.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax
+
+/-- The small-step reduction relation for System F<:. `Reduce e₁ e₂` means that
+    expression `e₁` can take a single computational step to become `e₂`. -/
+inductive Reduce : Exp s → Exp s → Prop where
+/-- Evaluate function position: if e₁ ⟶ e₁', then (e₁ e₂) ⟶ (e₁' e₂) -/
+| red_app_fun :
+  Reduce e1 e1' →
+  Reduce (.app e1 e2) (.app e1' e2)
+/-- Evaluate argument position: if v₁ is a value and e₂ ⟶ e₂', then (v₁ e₂) ⟶ (v₁ e₂') -/
+| red_app_arg :
+  Exp.IsVal v1 →
+  Reduce e2 e2' →
+  Reduce (.app v1 e2) (.app v1 e2')
+/-- Beta reduction: (λx:T.e₁) e₂ ⟶ e₁[x := e₂] -/
+| red_app :
+  Reduce (.app (.abs T e1) e2) (e1.open_var e2)
+/-- Evaluate polymorphic expression: if e ⟶ e', then (e [T]) ⟶ (e' [T]) -/
+| red_tapp_fun :
+  Reduce e e' →
+  Reduce (.tapp e T) (.tapp e' T)
+/-- Type application: (ΛX<:T'.e) [T] ⟶ e[X := T] -/
+| red_tapp :
+  Reduce (.tapp (.tabs T' e) T) (e.open_tvar T)
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean
new file mode 100644
index 00000000..3158b65a
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean
@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Retyping morphisms
+
+This module defines retyping morphisms, which are the second layer in the hierarchy
+of context morphisms for System F<:.
+Retyping morphisms extend rebinding morphisms by mapping variables to typing derivations
+rather than just renamed variables.
+
+A retyping morphism `ρ : Retype Γ σ Δ` consists of:
+- A parallel substitution `σ : s₁ → s₂`
+- Contexts `Γ : Ctx s₁` and `Δ : Ctx s₂`
+- Proofs that each variable in Γ maps to a well-typed term in Δ
+- Proofs that each type variable in Γ maps to a subtype in Δ
+
+More precisely, if `x : T ∈ Γ` then `Δ ⊢ σ(x) : σ(T)`,
+and if `X <: S ∈ Γ` then `Δ ⊢ σ(X) <: σ(S)`.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSystem
+
+/-- A retyping morphism `Retype Γ σ Δ` witnesses that contexts `Γ` and `Δ` are
+    related by the substitution `σ` in a type-preserving way.
+
+    Unlike rebinding morphisms, retyping morphisms map variables to typing derivations. -/
+structure Retype (Γ : Ctx s1) (σ : Subst s1 s2) (Δ : Ctx s2) where
+  var : ∀ x T,
+    (hb : Γ.LookupVar x T) →
+    HasType Δ (σ.var x) (T.subst σ)
+  tvar : ∀ X S,
+    (hb : Γ.LookupTVar X S) →
+    Subtyp Δ (σ.tvar X) (S.subst σ)
+
+/-- Extends a retyping morphism to contexts with an additional term variable. -/
+def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P.subst σ) where
+  var := fun x T hb => by
+    cases hb
+    case here =>
+      apply HasType.var
+      simp only [←Ty.subst_succVar_comm_base]
+      constructor
+    case there_var hb0 =>
+      have h0 := ρ.var _ _ hb0
+      simp only [←Ty.subst_succVar_comm_base]
+      apply h0.rebind Rebind.succVar
+  tvar := fun X S hb => by
+    cases hb
+    case there_var hb0 =>
+      have h0 := ρ.tvar _ _ hb0
+      simp only [←Ty.subst_succVar_comm_base]
+      apply h0.rebind Rebind.succVar
+
+/-- Extends a retyping morphism to contexts with an additional type variable. -/
+def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,X<:P.subst σ) where
+  var := fun x T hb => by
+    cases hb
+    case there_tvar hb0 =>
+      have h0 := ρ.var _ _ hb0
+      simp only [←Ty.subst_succTVar_comm_base]
+      apply h0.rebind Rebind.succTVar
+  tvar := fun X S hb => by
+    cases hb
+    case here =>
+      apply Subtyp.tvar
+      grind [Ty.subst_succTVar_comm_base]
+    case there_tvar hb0 =>
+      have h0 := ρ.tvar _ _ hb0
+      simp only [←Ty.subst_succTVar_comm_base]
+      apply h0.rebind Rebind.succTVar
+
+/-- Creates a retyping morphism that substitutes an expression for the newest term variable. -/
+def Retype.open_var
+  (ht : HasType Γ e T) :
+  Retype (Γ,x:T) (Subst.open_var e) Γ where
+  var := fun x T hb => by
+    cases hb
+    case here => simpa [Ty.rename_succVar_open_var]
+    case there_var hb0 => apply HasType.var; simpa [Ty.rename_succVar_open_var]
+  tvar := fun X S hb => by
+    cases hb
+    case there_var hb0 => apply Subtyp.tvar; simpa [Ty.rename_succVar_open_var]
+
+/-- Creates a retyping morphism that narrows the bound of the newest type variable. -/
+def Retype.narrow_tvar
+  (hs : Subtyp Γ S1 S2) :
+  Retype (Γ,X<:S2) Subst.id (Γ,X<:S1) where
+  var := fun x T hb => by cases hb; constructor; grind [Ty.subst_id]
+  tvar := fun X S hb => by
+    cases hb
+    case here =>
+      apply Subtyp.trans
+      · apply Subtyp.tvar; constructor
+      · simp only [Ty.subst_id]; apply hs.rebind Rebind.succTVar
+    case there_tvar hb0 => apply Subtyp.tvar; grind [Ty.subst_id]
+
+/-- Creates a retyping morphism that substitutes a type for the newest type variable. -/
+def Retype.open_tvar
+  (hs : Subtyp Γ R S) :
+  Retype (Γ,X<:S) (Subst.open_tvar R) Γ where
+  var := fun x T hb => by
+    cases hb
+    case there_tvar hb0 => apply HasType.var; grind [Ty.rename_succTVar_open_tvar]
+  tvar := fun X0 S0 hb => by
+    cases hb
+    case here => simpa [Ty.rename_succTVar_open_tvar]
+    case there_tvar hb0 => apply Subtyp.tvar; simpa [Ty.rename_succTVar_open_tvar]
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean
new file mode 100644
index 00000000..f5266c5c
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core
+
+/-- Context retyping preserves subtyping judgments. -/
+def Subtyp.retype {σ : Subst s1 s2}
+  (hsub : Subtyp Γ T1 T2)
+  (ρ : Retype Γ σ Δ) :
+  Subtyp Δ (T1.subst σ) (T2.subst σ) := by
+  induction hsub generalizing s2 <;> try (solve | constructor)
+  case trans ih1 ih2 => apply Subtyp.trans <;> aesop
+  case tvar hb => apply ρ.tvar _ _ hb
+  case arrow => apply arrow <;> aesop
+  case poly ih1 ih2 =>
+    apply poly <;> try grind
+    · apply ih2 ρ.liftTVar
+
+/-- Context retyping preserves typing judgments. -/
+theorem HasType.retype {σ : Subst s1 s2}
+  (ht : HasType Γ t T)
+  (ρ : Retype Γ σ Δ) :
+  HasType Δ (t.subst σ) (T.subst σ) := by
+  induction ht generalizing s2
+  case var hb => apply ρ.var _ _ hb
+  case sub hsub _ ih =>
+    apply sub <;> try aesop
+    apply hsub.retype ρ
+  case abs ih => apply HasType.abs; simpa [Ty.subst_succVar_comm_base] using ih ρ.liftVar
+  case tabs ih => apply HasType.tabs; apply ih ρ.liftTVar
+  case app ih1 ih2 => apply HasType.app <;> aesop
+  case tapp ih => simp only [Ty.open_tvar_subst_comm]; apply HasType.tapp; aesop
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean
new file mode 100644
index 00000000..a99da0f2
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Parallel substitution for System F<:
+
+This module provides the complete parallel substitution theory for System F<:.
+It imports both the core substitution definitions and their properties.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean
new file mode 100644
index 00000000..938b66e2
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Parallel substitution for System F<:
+
+This module defines parallel substitution operations, which allow simultaneous
+substitution of multiple variables.
+This provides a uniform way to handle variable binding and substitution.
+
+The module defines:
+- `Subst`: A parallel substitution that maps variables from signature s₁ to
+  expressions/types in signature s₂
+- Lifting operations that extend substitutions to work under binders
+- Opening operations for single-variable substitution
+- Identity substitution and conversion from renamings
+
+Parallel substitutions generalize both renamings and single-variable substitutions.
+The lifting operations extend substitutions to work under binders
+while respecting the scoping disciplines of the intrinsically scoped syntax.
+
+A substitution σ : s₁ → s₂ assigns to each variable x ∈ s₁ an expression σ(x)
+with variables in s₂, and to each type variable X ∈ s₁ a type σ(X) with variables in s₂.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core
+
+/-- A parallel substitution maps term variables to expressions and type variables
+    to types. This allows simultaneous substitution of multiple variables while
+    preserving well-scopedness. -/
+structure Subst (s1 s2 : Sig) where
+  /-- How to substitute term variables -/
+  var : Var s1 → Exp s2
+  /-- How to substitute type variables -/
+  tvar : TVar s1 → Ty s2
+
+/-- Lift a substitution to work under a term variable binder. The newly bound
+    variable is mapped to itself, while existing variables are substituted and
+    then weakened to account for the new binding. -/
+def Subst.liftVar (s : Subst s1 s2) : Subst (s1,x) (s2,x) where
+  var := fun x => match x with
+    | .here => .var .here
+    | .there_var x0 => (s.var x0).rename Rename.succVar
+  tvar := fun X => match X with
+    | .there_var X0 => (s.tvar X0).rename Rename.succVar
+
+/-- Lift a substitution to work under a type variable binder. The newly bound
+    type variable is mapped to itself, while existing variables are substituted
+    and then weakened to account for the new binding. -/
+def Subst.liftTVar (s : Subst s1 s2) : Subst (s1,X) (s2,X) where
+  tvar := fun X => match X with
+    | .here => .tvar .here
+    | .there_tvar X0 => (s.tvar X0).rename Rename.succTVar
+  var := fun x => match x with
+    | .there_tvar x0 => (s.var x0).rename Rename.succTVar
+
+/-- Create a substitution that replaces the outermost term variable with the given
+    expression, while leaving all other variables unchanged. This is used for
+    function application (beta reduction). -/
+def Subst.open_var (e : Exp s) : Subst (s,x) s where
+  var := fun x => match x with
+    | .here => e
+    | .there_var x0 => .var x0
+  tvar := fun X => match X with
+    | .there_var X0 => .tvar X0
+
+/-- Create a substitution that replaces the outermost type variable with the given
+    type, while leaving all other variables unchanged. This is used for
+    type application in polymorphic functions. -/
+def Subst.open_tvar (T : Ty s) : Subst (s,X) s where
+  var := fun x => match x with
+    | .there_tvar x0 => .var x0
+  tvar := fun X => match X with
+    | .here => T
+    | .there_tvar X0 => .tvar X0
+
+/-- Convert a renaming into a substitution. Every variable is mapped to the
+    correspondingly renamed variable. -/
+def Rename.asSubst (f : Rename s1 s2) : Subst s1 s2 where
+  var := fun x => .var (f.var x)
+  tvar := fun X => .tvar (f.tvar X)
+
+/-- Functional extensionality for substitutions: two substitutions are equal
+    if they map all variables in the same way. -/
+theorem Subst.funext {σ1 σ2 : Subst s1 s2}
+  (var : ∀ x, σ1.var x = σ2.var x)
+  (tvar : ∀ X, σ1.tvar X = σ2.tvar X) : σ1 = σ2 := by
+  cases σ1; cases σ2
+  aesop
+
+/-- Lift a substitution to work under multiple binders specified by a signature.
+    This generalizes `liftVar` and `liftTVar` to arbitrary sequences of binders. -/
+def Subst.lift : Subst s1 s2 → (s : Sig) → Subst (s1 ++ s) (s2 ++ s)
+| σ, .empty => σ
+| σ, .push_var s => (σ.lift s).liftVar
+| σ, .push_tvar s => (σ.lift s).liftTVar
+
+/-- The identity substitution that maps each variable to itself. -/
+def Subst.id : Subst s s where
+  var := fun x => .var x
+  tvar := fun X => .tvar X
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean
new file mode 100644
index 00000000..5a4aca5b
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean
@@ -0,0 +1,391 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Properties of parallel substitution for System F<:
+
+This module establishes the fundamental algebraic properties of parallel substitution
+that are essential for the metatheory of System F<:.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Subst
+
+/-- Composition of substitutions. If σ₁ maps s₁ to s₂ and σ₂ maps s₂ to s₃,
+    then their composition maps s₁ to s₃ by first applying σ₁ then σ₂. -/
+def Subst.comp (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : Subst s1 s3 where
+  var := fun x => (σ1.var x).subst σ2
+  tvar := fun X => (σ1.tvar X).subst σ2
+
+/-- Shows that lifting a substitution for term variables preserves type variable mappings
+    by renaming with succVar. -/
+theorem Subst.tvar_there_var_liftVar {σ : Subst s1 s2} :
+  (σ.liftVar.tvar (.there_var X)) = (σ.tvar X).rename Rename.succVar := rfl
+
+/-- Shows that lifting a substitution for type variables preserves older type variable mappings
+    by renaming with succTVar. -/
+theorem Subst.tvar_there_tvar_liftTVar {σ : Subst s1 s2} :
+  (σ.liftTVar.tvar (.there_tvar X)) = (σ.tvar X).rename Rename.succTVar := rfl
+
+/-- Shows that lifting a substitution for type variables preserves term variable mappings
+    by renaming with succTVar. -/
+theorem Subst.var_there_tvar_liftTVar {σ : Subst s1 s2} :
+  (σ.liftTVar.var (.there_tvar x)) = (σ.var x).rename Rename.succTVar := rfl
+
+/-- For type variables, substitution followed by term variable weakening equals
+    term variable weakening followed by substitution with a lifted substitution. -/
+theorem Ty.tvar_subst_succVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) :
+  ((tvar X).subst (σ.lift s0)).rename (Rename.succVar.lift s0) =
+    ((tvar X).rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by
+  induction s0
+  case empty => rfl
+  case push_var s0 ih =>
+    cases X
+    case there_var X0 =>
+      simp only [Subst.lift, Ty.subst]
+      conv => lhs; simp only [Subst.liftVar]
+      conv => rhs; simp only [Subst.tvar_there_var_liftVar]
+      simp only [Rename.lift, ←Ty.rename_succVar_comm]
+      congr; exact (ih (X:=X0))
+  case push_tvar s0 ih =>
+    cases X <;> try rfl
+    case there_tvar X0 =>
+      conv => lhs; simp only [Subst.lift, Ty.subst]
+      conv => lhs; simp only [Subst.liftTVar, Rename.lift]
+      simp only [←Ty.rename_succTVar_comm]
+      congr; exact (ih (X:=X0))
+
+/-- Proves that substitution commutes with type variable weakening for type variables. -/
+theorem Ty.tvar_subst_succTVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) :
+  ((tvar X).subst (σ.lift s0)).rename (Rename.succTVar.lift s0) =
+    ((tvar X).rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by
+  induction s0
+  case empty => rfl
+  case push_var s0 ih =>
+    cases X
+    case there_var X0 =>
+      conv => lhs; simp only [Subst.lift, Ty.subst]
+      conv => lhs; simp only [Subst.liftVar, Rename.lift]
+      simp only [←Ty.rename_succVar_comm]
+      congr; exact (ih (X:=X0))
+  case push_tvar s0 ih =>
+    cases X <;> try rfl
+    case there_tvar X0 =>
+      conv => lhs; simp only [Subst.lift, Ty.subst]
+      conv => lhs; simp only [Subst.liftTVar, Rename.lift]
+      simp only [←Ty.rename_succTVar_comm]
+      congr; exact (ih (X:=X0))
+
+/-- Proves that substitution commutes with term variable weakening for types. -/
+theorem Ty.subst_succVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) :
+  (T.subst (σ.lift s0)).rename (Rename.succVar.lift s0) =
+    (T.rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by
+  match T with
+  | .top => rfl
+  | .tvar X => simp [Ty.tvar_subst_succVar_comm]
+  | .arrow T1 T2 =>
+    have ih1 := Ty.subst_succVar_comm (T:=T1) (σ:=σ)
+    have ih2 := Ty.subst_succVar_comm (T:=T2) (σ:=σ)
+    grind [Ty.subst, Ty.rename]
+  | .poly T1 T2 =>
+    have ih1 := Ty.subst_succVar_comm (T:=T1) (σ:=σ)
+    have ih2 := Ty.subst_succVar_comm (s0:=s0,X) (T:=T2) (σ:=σ)
+    simpa [Ty.subst, Ty.rename, ih1]
+
+/-- Proves that substitution commutes with type variable weakening for types. -/
+theorem Ty.subst_succTVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) :
+  (T.subst (σ.lift s0)).rename (Rename.succTVar.lift s0) =
+    (T.rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by
+  match T with
+  | .top => rfl
+  | .tvar X => simp [Ty.tvar_subst_succTVar_comm]
+  | .arrow T1 T2 =>
+    have ih1 := Ty.subst_succTVar_comm (T:=T1) (σ:=σ)
+    have ih2 := Ty.subst_succTVar_comm (T:=T2) (σ:=σ)
+    grind [Ty.subst, Ty.rename]
+  | .poly T1 T2 =>
+    have ih1 := Ty.subst_succTVar_comm (T:=T1) (σ:=σ)
+    have ih2 := Ty.subst_succTVar_comm (s0:=s0,X) (T:=T2) (σ:=σ)
+    simpa [Ty.subst, Ty.rename, ih1]
+
+/-- Base case of substitution commuting with term variable weakening. -/
+theorem Ty.subst_succVar_comm_base {T : Ty s1} (σ : Subst s1 s2) :
+  (T.subst σ).rename Rename.succVar = (T.rename Rename.succVar).subst (σ.liftVar) := by
+  exact Ty.subst_succVar_comm (T:=T) (σ:=σ) (s0:=Sig.empty)
+
+/-- Base case of substitution commuting with type variable weakening. -/
+theorem Ty.subst_succTVar_comm_base {T : Ty s1} (σ : Subst s1 s2) :
+  (T.subst σ).rename Rename.succTVar = (T.rename Rename.succTVar).subst (σ.liftTVar) := by
+  exact Ty.subst_succTVar_comm (T:=T) (σ:=σ) (s0:=Sig.empty)
+
+/-- Shows that renaming an expression commutes with type variable weakening. -/
+theorem Exp.rename_succTVar_comm {e : Exp s1} {f : Rename s1 s2} :
+  (e.rename f).rename Rename.succTVar =
+    (e.rename Rename.succTVar).rename f.liftTVar := by
+  simp [Exp.rename_comp, Rename.rename_succTVar_comm]
+
+/-- Shows that renaming an expression commutes with term variable weakening. -/
+theorem Exp.rename_succVar_comm {e : Exp s1} {f : Rename s1 s2} :
+  (e.rename f).rename Rename.succVar =
+    (e.rename Rename.succVar).rename f.liftVar := by
+  simp [Exp.rename_comp, Rename.rename_succVar_comm]
+
+/-- Proves that substitution commutes with type variable weakening for variables. -/
+theorem Exp.var_subst_succTVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) :
+  ((var x).subst (σ.lift s0)).rename (Rename.succTVar.lift s0) =
+    ((var x).rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by
+  induction s0 <;> try rfl
+  case push_var s0 ih =>
+    cases x <;> try rfl
+    case there_var x0 =>
+      conv => lhs; simp only [Subst.lift, Exp.subst]
+      conv => lhs; simp only [Subst.liftVar, Rename.lift]
+      simp only [←Exp.rename_succVar_comm]
+      congr; exact (ih (x:=x0))
+  case push_tvar s0 ih =>
+    cases x
+    case there_tvar x0 =>
+      conv => lhs; simp only [Subst.liftVar, Subst.lift, Rename.lift]
+      conv => lhs; simp only [Exp.subst, Subst.liftTVar]
+      simp only [←Exp.rename_succTVar_comm]
+      congr; exact (ih (x:=x0))
+
+/-- Proves that substitution commutes with term variable weakening for variables. -/
+theorem Exp.var_subst_succVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) :
+  ((var x).subst (σ.lift s0)).rename (Rename.succVar.lift s0) =
+    ((var x).rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by
+  induction s0 <;> try rfl
+  case push_var s0 ih =>
+    cases x <;> try rfl
+    case there_var x0 =>
+      conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift]
+      simp only [←Exp.rename_succVar_comm]
+      congr; exact (ih (x:=x0))
+  case push_tvar s0 ih =>
+    cases x
+    case there_tvar x0 =>
+      conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift]
+      simp only [←Exp.rename_succTVar_comm]
+      congr; exact (ih (x:=x0))
+
+/-- Proves that substitution commutes with type variable weakening for expressions. -/
+theorem Exp.subst_succTVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) :
+  (e.subst (σ.lift s0)).rename (Rename.succTVar.lift s0) =
+    (e.rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by
+  match e with
+  | .var x => simp [Exp.var_subst_succTVar_comm]
+  | .abs A t =>
+    have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ)
+    have ih2 := Exp.subst_succTVar_comm (s0:=s0,x) (e:=t) (σ:=σ)
+    simp only [Exp.subst, Exp.rename, ih1]; congr
+  | .tabs A t =>
+    have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ)
+    have ih2 := Exp.subst_succTVar_comm (s0:=s0,X) (e:=t) (σ:=σ)
+    simp only [Exp.subst, Exp.rename, ih1]; congr
+  | .app t1 t2 =>
+    have ih1 := Exp.subst_succTVar_comm (e:=t1) (σ:=σ)
+    have ih2 := Exp.subst_succTVar_comm (e:=t2) (σ:=σ)
+    simp [Exp.subst, Exp.rename, ih1, ih2]
+  | .tapp t A =>
+    have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ)
+    have ih2 := Exp.subst_succTVar_comm (s0:=s0) (e:=t) (σ:=σ)
+    simp [Exp.subst, Exp.rename, ih1, ih2]
+
+/-- Proves that substitution commutes with term variable weakening for expressions. -/
+theorem Exp.subst_succVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) :
+  (e.subst (σ.lift s0)).rename (Rename.succVar.lift s0) =
+    (e.rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by
+  match e with
+  | .var x => simp [Exp.var_subst_succVar_comm]
+  | .abs A t =>
+    have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ)
+    have ih2 := Exp.subst_succVar_comm (s0:=s0,x) (e:=t) (σ:=σ)
+    simp only [Exp.subst, Exp.rename, ih1]; congr
+  | .tabs A t =>
+    have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ)
+    have ih2 := Exp.subst_succVar_comm (s0:=s0,X) (e:=t) (σ:=σ)
+    simp only [Exp.subst, Exp.rename, ih1]; congr
+  | .app t1 t2 =>
+    have ih1 := Exp.subst_succVar_comm (e:=t1) (σ:=σ)
+    have ih2 := Exp.subst_succVar_comm (e:=t2) (σ:=σ)
+    simp [Exp.subst, Exp.rename, ih1, ih2]
+  | .tapp t A =>
+    have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ)
+    have ih2 := Exp.subst_succVar_comm (s0:=s0) (e:=t) (σ:=σ)
+    simp [Exp.subst, Exp.rename, ih1, ih2]
+
+/-- Proves that lifting a substitution for type variables commutes with composition. -/
+theorem Subst.liftTVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} :
+  (σ1.comp σ2).liftTVar = σ1.liftTVar.comp σ2.liftTVar := by
+  apply Subst.funext
+  case var =>
+    intro x; cases x
+    case there_tvar x0 =>
+      simp [Subst.comp, Subst.liftTVar]
+      simpa [Subst.lift, Rename.lift] using
+        (Exp.subst_succTVar_comm (s0:=Sig.empty) (σ:=σ2))
+  case tvar =>
+    intro X; cases X <;> try rfl
+    case there_tvar X0 =>
+      simpa [Subst.lift, Rename.lift] using
+        (Ty.subst_succTVar_comm (s0:=Sig.empty) (T:=σ1.tvar X0) (σ:=σ2))
+
+/-- Proves that lifting a substitution for term variables commutes with composition. -/
+theorem Subst.liftVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} :
+  (σ1.comp σ2).liftVar = σ1.liftVar.comp σ2.liftVar := by
+  apply Subst.funext
+  case var =>
+    intro x; cases x <;> try rfl
+    case there_var x0 =>
+      simpa [Subst.lift, Rename.lift] using
+        (Exp.subst_succVar_comm (s0:=Sig.empty) (σ:=σ2))
+  case tvar =>
+    intro X; cases X
+    case there_var X0 =>
+      simpa [Subst.lift, Rename.lift] using
+        (Ty.subst_succVar_comm (s0:=Sig.empty) (T:=σ1.tvar X0) (σ:=σ2))
+
+/-- **Fundamental associativity law for substitution composition on types**:
+    Sequential application of substitutions equals composition.
+
+    This states that (T[σ₁])[σ₂] = T[σ₁ ∘ σ₂], establishing that substitution
+    forms a category-like structure. This is essential for reasoning about
+    complex substitution chains in proofs. -/
+theorem Ty.subst_comp {T : Ty s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) :
+  (T.subst σ1).subst σ2 = T.subst (σ1.comp σ2) := by
+  induction T generalizing s2 s3 <;> try (solve | rfl)
+  all_goals simp only [Ty.subst, Subst.liftTVar_comp]; grind
+
+/-- **Fundamental associativity law for substitution composition on expressions**:
+    Sequential application of substitutions equals composition.
+
+    This extends the associativity property to expressions, ensuring that
+    the substitution algebra is consistent across all syntactic categories. -/
+theorem Exp.subst_comp {e : Exp s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) :
+  (e.subst σ1).subst σ2 = e.subst (σ1.comp σ2) := by
+  induction e generalizing s2 s3
+  case var x => rfl
+  all_goals grind [Exp.subst, Ty.subst_comp, Subst.liftVar_comp, Subst.liftTVar_comp]
+
+/-- Shows that converting a rename to a substitution commutes with lifting for type variables. -/
+theorem Rename.asSubst_liftTVar_comm {f : Rename s1 s2} :
+  (f.asSubst).liftTVar = f.liftTVar.asSubst := by
+  apply Subst.funext <;> intro a <;> cases a <;> rfl
+
+/-- Shows that converting a rename to a substitution commutes with lifting for term variables. -/
+theorem Rename.asSubst_liftVar_comm {f : Rename s1 s2} :
+  (f.asSubst).liftVar = f.liftVar.asSubst := by
+  apply Subst.funext <;> intro a <;> cases a <;> rfl
+
+/-- Proves that substituting with a rename-as-substitution equals renaming for types. -/
+theorem Ty.subst_asSubst {T : Ty s1} {f : Rename s1 s2} :
+  T.subst f.asSubst = T.rename f := by
+  induction T generalizing s2
+    <;> try (solve | rfl | grind [Ty.subst, Ty.rename, Rename.asSubst_liftTVar_comm])
+
+/-- Proves that substituting with a rename-as-substitution equals renaming for expressions. -/
+theorem Exp.subst_asSubst {e : Exp s1} {f : Rename s1 s2} :
+  e.subst f.asSubst = e.rename f := by
+  induction e generalizing s2
+  case var x => rfl
+  all_goals (simp only [Exp.subst, Exp.rename,
+    Ty.subst_asSubst, Rename.asSubst_liftVar_comm, Rename.asSubst_liftTVar_comm]; grind)
+
+/-- Shows that lifting the identity substitution for term variables gives the identity. -/
+theorem Subst.id_liftVar :
+  (Subst.id (s:=s)).liftVar = Subst.id := by
+  apply Subst.funext <;> intro a <;> cases a <;> rfl
+
+/-- Shows that lifting the identity substitution for type variables gives the identity. -/
+theorem Subst.id_liftTVar :
+  (Subst.id (s:=s)).liftTVar = Subst.id := by
+  apply Subst.funext <;> intro a <;> cases a <;> rfl
+
+/-- **Identity law for types**: The identity substitution acts as neutral element.
+    This establishes that T[id] = T, showing that substitution has the proper
+    categorical structure with identity morphisms. -/
+theorem Ty.subst_id {T : Ty s} : T.subst Subst.id = T := by
+  induction T <;> try (solve | rfl)
+  all_goals (simp only [Ty.subst, Subst.id_liftTVar]; grind)
+
+/-- **Identity law for expressions**: The identity substitution acts as neutral element.
+    This extends the identity property to expressions, completing the algebraic
+    structure of the substitution category. -/
+theorem Exp.subst_id {e : Exp s} : e.subst Subst.id = e := by
+  induction e <;> try (solve | rfl)
+  all_goals (simp only [Exp.subst, Ty.subst_id, Subst.id_liftVar, Subst.id_liftTVar]; grind)
+
+/-- Proves that opening a type variable commutes with renaming for substitutions. -/
+theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} :
+  (Subst.open_tvar T).comp (f.asSubst)
+    = f.liftTVar.asSubst.comp (Subst.open_tvar (T.rename f)) := by
+  apply Subst.funext
+  case var => intro x; cases x; rfl
+  case tvar =>
+    intro X; cases X <;> try (solve | rfl | simp only [Subst.comp, Ty.subst_asSubst]; rfl)
+
+/-- Proves that opening a type variable commutes with renaming for types. -/
+theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} :
+  (T.open_tvar U).rename f = (T.rename f.liftTVar).open_tvar (U.rename f) := by
+  simp only [Ty.open_tvar, ←Ty.subst_asSubst]
+  grind [Ty.subst_comp, Subst.open_tvar_rename_comm, Ty.subst_asSubst]
+
+/-- Shows that successively weakening then opening a type variable gives the identity. -/
+theorem Subst.succTVar_open_tvar {T : Ty s} :
+  Rename.succTVar.asSubst.comp (Subst.open_tvar T) = Subst.id := by apply Subst.funext <;> aesop
+
+/-- Proves that renaming with succTVar then opening cancels out for expressions. -/
+theorem Exp.rename_succTVar_open_tvar {e : Exp s} :
+  (e.rename Rename.succTVar).subst (Subst.open_tvar X) =
+    e := by
+  simp only [←Exp.subst_asSubst]
+  grind [Exp.subst_comp, Subst.succTVar_open_tvar, Exp.subst_id]
+
+/-- Proves that renaming with succTVar then opening cancels out for types. -/
+theorem Ty.rename_succTVar_open_tvar {T : Ty s} :
+  (T.rename Rename.succTVar).subst (Subst.open_tvar X) =
+    T := by
+  simp only [←Ty.subst_asSubst]
+  grind [Ty.subst_comp, Subst.succTVar_open_tvar, Ty.subst_id]
+
+/-- Shows that successively weakening then opening a term variable gives the identity. -/
+theorem Subst.succVar_open_var {e : Exp s} :
+  Rename.succVar.asSubst.comp (Subst.open_var e) = Subst.id := by apply Subst.funext <;> aesop
+
+/-- Proves that renaming with succVar then opening cancels out for expressions. -/
+theorem Exp.rename_succVar_open_var {e : Exp s} :
+  (e.rename Rename.succVar).subst (Subst.open_var X) =
+    e := by
+  simp only [←Exp.subst_asSubst]
+  grind [Exp.subst_comp, Subst.succVar_open_var, Exp.subst_id]
+
+/-- Proves that renaming with succVar then opening cancels out for types. -/
+theorem Ty.rename_succVar_open_var {T : Ty s} :
+  (T.rename Rename.succVar).subst (Subst.open_var X) =
+    T := by
+  simp only [←Ty.subst_asSubst]
+  grind [Ty.subst_comp, Subst.succVar_open_var, Ty.subst_id]
+
+/-- Proves that opening a type variable commutes with substitution for substitutions. -/
+theorem Subst.open_tvar_subst_comm {T : Ty s} {σ : Subst s s'} :
+  (Subst.open_tvar T).comp σ = σ.liftTVar.comp (Subst.open_tvar (T.subst σ)) := by
+  apply Subst.funext
+  case var =>
+    intro x; cases x
+    conv => lhs; simp only [Subst.comp, Subst.open_tvar]
+    conv => rhs; simp only [Subst.comp, Subst.liftTVar]
+    simp only [Exp.rename_succTVar_open_tvar]; rfl
+  case tvar =>
+    intro X; cases X <;> try rfl
+    case there_tvar X0 =>
+      conv => lhs; simp only [Subst.comp, Subst.open_tvar]
+      conv => rhs; simp only [Subst.comp, Subst.liftTVar]
+      simp only [Ty.rename_succTVar_open_tvar]; rfl
+
+/-- Proves that opening a type variable commutes with substitution for types. -/
+theorem Ty.open_tvar_subst_comm {T : Ty (s,X)} {U : Ty s} {σ : Subst s s'} :
+  (T.open_tvar U).subst σ = (T.subst σ.liftTVar).open_tvar (U.subst σ) := by
+  simp [Ty.open_tvar, Ty.subst_comp, Subst.open_tvar_subst_comm]
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean
new file mode 100644
index 00000000..520f87af
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# System F<: syntax
+
+This module aggregates all the syntactic components of System F<:.
+
+## Components:
+- `Core`: Basic types and expressions with their renaming operations
+- `Context`: Typing contexts and variable lookup relations
+- `Subst`: Substitution operations and their lifting under binders
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Context
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Subst
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean
new file mode 100644
index 00000000..577a7717
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Typing contexts for System F<:
+
+This module defines typing contexts and variable lookup relations for System F<:.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core
+
+/-- A typing context assigns types to term variables and upper bounds to type variables. -/
+inductive Ctx : Sig → Type where
+/-- Empty context -/
+| empty : Ctx {}
+/-- Extend with term variable x : T -/
+| cons_var : Ctx s → Ty s → Ctx (s,x)
+/-- Extend with type variable X <: T -/
+| cons_tvar : Ctx s → Ty s → Ctx (s,X)
+
+/-- Convenient notation for extending context with a term variable -/
+infixl:50 ",x:" => Ctx.cons_var
+/-- Convenient notation for extending context with a type variable -/
+infixl:50 ",X<:" => Ctx.cons_tvar
+
+/-- Variable lookup relation. `Ctx.LookupVar Γ x T` means that term variable `x`
+    has type `T` in context `Γ`. -/
+@[grind]
+inductive Ctx.LookupVar : Ctx s → Var s → Ty s → Prop where
+/-- Look up the most recently bound term variable -/
+| here :
+  Ctx.LookupVar (Γ,x:T) .here (T.rename Rename.succVar)
+/-- Skip over a more recent term variable binding -/
+| there_var :
+  Ctx.LookupVar Γ x T →
+  Ctx.LookupVar (Γ,x:U) (x.there_var) (T.rename Rename.succVar)
+/-- Skip over a more recent type variable binding -/
+| there_tvar :
+  Ctx.LookupVar Γ x T →
+  Ctx.LookupVar (Γ,X<:S) (x.there_tvar) (T.rename Rename.succTVar)
+
+/-- Type variable lookup relation. `Ctx.LookupTVar Γ X T` means that type variable `X`
+    has upper bound `T` in context `Γ`. -/
+@[grind]
+inductive Ctx.LookupTVar : Ctx s → TVar s → Ty s → Prop where
+/-- Look up the most recently bound type variable -/
+| here :
+  Ctx.LookupTVar (Γ,X<:T) .here (T.rename Rename.succTVar)
+/-- Skip over a more recent term variable binding -/
+| there_var :
+  Ctx.LookupTVar Γ X T →
+  Ctx.LookupTVar (Γ,x:U) X.there_var (T.rename Rename.succVar)
+/-- Skip over a more recent type variable binding -/
+| there_tvar :
+  Ctx.LookupTVar Γ X T →
+  Ctx.LookupTVar (Γ,X<:S) X.there_tvar (T.rename Rename.succTVar)
+
+@[simp]
+instance : EmptyCollection (Ctx {}) := ⟨Ctx.empty⟩
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean
new file mode 100644
index 00000000..652c6971
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Core syntax for System F<:
+
+This module defines the core syntactic constructs of System F<: (System F with subtyping).
+The syntax uses intrinsically scoped de Bruijn indices where variables are indexed by
+signatures that ensure well-scopedness by construction.
+
+The module defines:
+- `Ty`: Types including top type, type variables, function types, and polymorphic types
+- `Exp`: Expressions including variables, abstractions, applications, and type applications
+- Renaming operations for both types and expressions
+- Value predicate identifying syntactic values
+
+The syntax is intrinsically well-scoped.
+Variables cannot refer to bindings that don't exist.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Debruijn
+
+/-- Types in System F<:. The type system includes:
+    - `top`: The universal supertype that all types are subtypes of
+    - `tvar`: Type variables, intrinsically scoped by signature
+    - `arrow`: Function types (A → B)
+    - `poly`: Polymorphic types (forall X <: A. B) where B has access to type variable X -/
+inductive Ty : Sig → Type where
+/-- The top type, supertype of all types -/
+| top : Ty s
+/-- Type variable -/
+| tvar : TVar s → Ty s
+/-- Function type A → B -/
+| arrow : Ty s → Ty s → Ty s
+/-- Polymorphic type ∀X<:A.B -/
+| poly : Ty s → Ty (s,X) → Ty s
+
+/-- Rename all type variables in a type according to the given renaming. -/
+def Ty.rename : Ty s1 → Rename s1 s2 → Ty s2
+| top, _ => top
+| tvar X, ρ => tvar (ρ.tvar X)
+| arrow A B, ρ => arrow (A.rename ρ) (B.rename ρ)
+| poly A B, ρ => poly (A.rename ρ) (B.rename ρ.liftTVar)
+
+/-- Expressions in System F<:. The expression language includes:
+    - `var`: Term variables, intrinsically scoped
+    - `abs`: Function abstraction (λx:T. e) where T is the parameter type
+    - `tabs`: Type abstraction (ΛX<:T. e) for polymorphic functions
+    - `app`: Function application (e₁ e₂)
+    - `tapp`: Type application (e T) for instantiating polymorphic functions -/
+inductive Exp : Sig → Type where
+/-- Term variable -/
+| var : Var s → Exp s
+/-- Function abstraction λx:T.e -/
+| abs : Ty s → Exp (s,x) → Exp s
+/-- Type abstraction ΛX<:T.e -/
+| tabs : Ty s → Exp (s,X) → Exp s
+/-- Function application e₁ e₂ -/
+| app : Exp s → Exp s → Exp s
+/-- Type application e[T] -/
+| tapp : Exp s → Ty s → Exp s
+
+/-- Rename all variables (both term and type variables) in an expression
+    according to the given renaming. -/
+def Exp.rename : Exp s1 → Rename s1 s2 → Exp s2
+| var x, ρ => var (ρ.var x)
+| abs A e, ρ => abs (A.rename ρ) (e.rename ρ.liftVar)
+| tabs A e, ρ => tabs (A.rename ρ) (e.rename ρ.liftTVar)
+| app e1 e2, ρ => app (e1.rename ρ) (e2.rename ρ)
+| tapp e A, ρ => tapp (e.rename ρ) (A.rename ρ)
+
+/-- Renaming with the identity renaming leaves a type unchanged. -/
+theorem Ty.rename_id {T : Ty s} : T.rename Rename.id = T := by
+  induction T <;> try (solve | rfl | simp only [Ty.rename, Rename.id_liftTVar_eq_id]; grind)
+
+/-- Renaming with the identity renaming leaves an expression unchanged. -/
+theorem Exp.rename_id {e : Exp s} : e.rename Rename.id = e := by
+  induction e <;> try (solve | rfl |
+    simp only [Exp.rename, Ty.rename_id, Rename.id_liftVar_eq_id, Rename.id_liftTVar_eq_id]; grind)
+
+/-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/
+theorem Ty.rename_comp {T : Ty s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} :
+  (T.rename f1).rename f2 = T.rename (f1.comp f2) := by
+  induction T generalizing s2 s3 <;>
+    try (solve | rfl | simp only [Ty.rename, Rename.comp_liftTVar]; grind)
+
+/-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/
+theorem Exp.rename_comp {e : Exp s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} :
+  (e.rename f1).rename f2 = e.rename (f1.comp f2) := by
+  induction e generalizing s2 s3 <;>
+    try (solve | rfl)
+  all_goals
+    simp only [Exp.rename, Ty.rename_comp, Rename.comp_liftVar, Rename.comp_liftTVar]; grind
+
+/-- Commutativity law for term variable weakening and general renamings. -/
+theorem Ty.rename_succVar_comm {T : Ty s} :
+  (T.rename f).rename Rename.succVar = (T.rename Rename.succVar).rename f.liftVar := by
+  simp [Ty.rename_comp, Rename.rename_succVar_comm]
+
+/-- Commutativity law for type variable weakening and general renamings. -/
+theorem Ty.rename_succTVar_comm {T : Ty s} :
+  (T.rename f).rename Rename.succTVar = (T.rename Rename.succTVar).rename f.liftTVar := by
+  simp [Ty.rename_comp, Rename.rename_succTVar_comm]
+
+/-- The value predicate identifies expressions that are syntactic values.
+    In System F<:, values are function abstractions and type abstractions.
+    This predicate is used in the operational semantics to determine when
+    evaluation has reached a final result. -/
+@[grind]
+inductive Exp.IsVal : Exp s → Prop where
+/-- Function abstractions are values -/
+| abs : IsVal (.abs T e)
+/-- Type abstractions are values -/
+| tabs : IsVal (.tabs T e)
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean
new file mode 100644
index 00000000..0c4bcfb3
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Substitution operations for System F<: syntax
+
+This module defines substitution operations for types and expressions in System F<:.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core
+
+/-- Apply a parallel substitution to a type. -/
+def Ty.subst : Ty s1 → Subst s1 s2 → Ty s2
+| .top, _ => .top
+| .tvar X, s => s.tvar X
+| .arrow A B, s => .arrow (A.subst s) (B.subst s)
+| .poly A B, s => .poly (A.subst s) (B.subst s.liftTVar)
+
+/-- Apply a parallel substitution to an expression. -/
+def Exp.subst : Exp s1 → Subst s1 s2 → Exp s2
+| .var x, s => s.var x
+| .abs A e, s => .abs (A.subst s) (e.subst s.liftVar)
+| .tabs A e, s => .tabs (A.subst s) (e.subst s.liftTVar)
+| .app e1 e2, s => .app (e1.subst s) (e2.subst s)
+| .tapp e A, s => .tapp (e.subst s) (A.subst s)
+
+/-- Substitute a concrete type for the outermost type variable in a polymorphic type. -/
+def Ty.open_tvar (T : Ty (s,X)) (U : Ty s) : Ty s :=
+  T.subst (Subst.open_tvar U)
+
+/-- Substitute a concrete expression for the outermost term variable in an expression. -/
+def Exp.open_var (e : Exp (s,x)) (U : Exp s) : Exp s :=
+  e.subst (Subst.open_var U)
+
+/-- Substitute a concrete type for the outermost type variable in an expression. -/
+def Exp.open_tvar (e : Exp (s,X)) (U : Ty s) : Exp s :=
+  e.subst (Subst.open_tvar U)
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean
new file mode 100644
index 00000000..d10351c1
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean
@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Canonical forms lemmas for System F<:
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem
+
+/-- Predicate for empty contexts -/
+inductive Ctx.IsEmpty : Ctx s → Prop where
+| empty_is_empty : Ctx.IsEmpty .empty
+
+theorem HasType.app_inv
+  (ht : HasType Γ (.app e1 e2) T) :
+  ∃ T1 T2,
+    HasType Γ e1 (.arrow T1 T2) ∧ HasType Γ e2 T1 ∧ Subtyp Γ T2 T := by
+  generalize he0 : Exp.app e1 e2 = e at ht
+  induction ht <;> cases he0 <;> grind
+
+theorem Subtyp.top_inv
+  (hsub : Subtyp Γ .top T) :
+  T = .top := by
+  generalize he0 : Ty.top = T at hsub
+  induction hsub <;> cases he0 <;> try (solve | rfl | aesop)
+
+theorem Subtyp.arrow_inv_left
+  (hsub : Subtyp Γ (.arrow T1 U1) T) :
+  (∃ T2 U2, T = .arrow T2 U2) ∨ T = .top := by
+  generalize he0 : Ty.arrow T1 U1 = T at hsub
+  induction hsub <;> cases he0 <;> try (solve | rfl | aesop)
+  case trans ih1 _ ih2 =>
+    cases (ih2 rfl)
+    case inl ih2 => aesop
+    case inr ih2 => cases ih2; grind [Subtyp.top_inv]
+
+theorem Subtyp.poly_inv_left
+  (hsub : Subtyp Γ (.poly T1 T2) T) :
+  (∃ T3 T4, T = .poly T3 T4) ∨ T = .top := by
+  generalize he0 : Ty.poly T1 T2 = T at hsub
+  induction hsub <;> cases he0 <;> try (solve | aesop)
+  case trans ih1 _ ih2 =>
+    cases (ih2 rfl)
+    case inl ih2 => aesop
+    case inr ih2 => cases ih2; grind [Subtyp.top_inv]
+
+theorem Subtype.tvar_inv_right
+  (hsub : Subtyp Γ T (.tvar X)) :
+  ∃ X0, T = .tvar X0 := by
+  generalize he0 : Ty.tvar X = T0 at hsub
+  induction hsub <;> cases he0 <;> try (solve | aesop)
+
+theorem Subtyp.arrow_inv_right
+  (hsub : Subtyp Γ T (.arrow T2 U2)) :
+  (∃ T1 U1, T = .arrow T1 U1) ∨ (∃ X, T = .tvar X) := by
+  generalize he0 : Ty.arrow T2 U2 = T0 at hsub
+  induction hsub <;> cases he0 <;> try (solve | aesop)
+  case trans ih1 _ ih2 =>
+    cases (ih2 rfl)
+    case inl ih2 =>
+      have ⟨T2, U2, h⟩ := ih2
+      cases h; specialize ih1 rfl; grind
+    case inr ih2 =>
+      have ⟨X, h⟩ := ih2; cases h; rename_i hsub _ _
+      have := Subtype.tvar_inv_right hsub; grind
+
+theorem Subtyp.poly_inv_right
+  (hsub : Subtyp Γ T (.poly T2 U2)) :
+  (∃ T1 U1, T = .poly T1 U1) ∨ (∃ X, T = .tvar X) := by
+  generalize he0 : Ty.poly T2 U2 = T0 at hsub
+  induction hsub <;> cases he0 <;> try (solve | aesop)
+  case trans ih1 _ ih2 =>
+    cases (ih2 rfl)
+    case inl ih2 => have ⟨T2, U2, h⟩ := ih2; cases h; grind
+    case inr ih2 =>
+      have ⟨X, h⟩ := ih2; cases h
+      rename_i hsub _ _
+      have := Subtype.tvar_inv_right hsub; grind
+
+theorem Subtyp.arrow_inv
+  (hsub : Subtyp Γ (.arrow T1 U1) (.arrow T2 U2)) :
+  Subtyp Γ T2 T1 ∧ Subtyp Γ U1 U2 := by
+  generalize he1 : Ty.arrow T1 U1 = P1 at hsub
+  generalize he2 : Ty.arrow T2 U2 = P2 at hsub
+  induction hsub <;> cases he1 <;> cases he2
+  case refl => constructor <;> apply Subtyp.refl
+  case arrow => aesop
+  case trans hs1 ih1 hs2 ih2 => cases (Subtyp.arrow_inv_left hs1) <;> grind [Subtyp.top_inv]
+
+theorem Subtyp.poly_inv
+  (hsub : Subtyp Γ (.poly T1 U1) (.poly T2 U2)) :
+  Subtyp Γ T2 T1 ∧ Subtyp (Γ,X<:T2) U1 U2 := by
+  generalize he1 : Ty.poly T1 U1 = P1 at hsub
+  generalize he2 : Ty.poly T2 U2 = P2 at hsub
+  induction hsub <;> cases he1 <;> cases he2
+  case refl => constructor <;> apply Subtyp.refl
+  case poly => aesop
+  case trans hs1 ih1 hs2 ih2 =>
+    cases (Subtyp.poly_inv_left hs1)
+    case inl h =>
+      have ⟨T3, T4, h⟩ := h; cases h
+      have ⟨ih11, ih12⟩ := ih1 rfl rfl; have ⟨ih21, ih22⟩ := ih2 rfl rfl
+      constructor
+      · grind
+      · have ih12' := ih12.retype (Retype.narrow_tvar ih21)
+        grind [Ty.subst_id]
+    case inr h => cases h; grind [Subtyp.top_inv]
+
+theorem Subtyp.non_tvar_left_inv
+  (hsub : Subtyp Γ T1 T2)
+  (hnt : ∀ X, T1 ≠ .tvar X) :
+  ∀ X, T2 ≠ .tvar X := by
+  induction hsub <;> try (solve | aesop)
+
+theorem HasType.value_typing
+  (hv : Exp.IsVal v)
+  (ht : HasType Γ v T) :
+  ∀ X, T ≠ .tvar X := by
+  induction ht <;> try (solve | cases hv | aesop)
+  case sub hsub _ _ => apply Subtyp.non_tvar_left_inv hsub; aesop
+
+theorem HasType.abs_inv {Γ : Ctx s}
+  (ht : HasType Γ (.abs T0 e) (.arrow T1 U1)) :
+  ∃ U0,
+    HasType (Γ,x:T0) e (U0.rename Rename.succVar) ∧
+    Subtyp Γ T1 T0 ∧
+    Subtyp Γ U0 U1 := by
+  generalize he1 : Exp.abs T0 e = t at ht
+  generalize he2 : Ty.arrow T1 U1 = P at ht
+  induction ht <;> cases he1 <;> cases he2
+  case abs T0 t0 U0 ht _ => use U0; split_ands <;> grind
+  case sub hsub =>
+    cases (Subtyp.arrow_inv_right hsub)
+    case inl h => have ⟨T1, U1, h⟩ := h; cases h; grind [Subtyp.arrow_inv]
+    case inr h => grind [HasType.value_typing]
+
+theorem HasType.tapp_inv
+  (ht : HasType Γ (.tapp e T) U) :
+  ∃ T2,
+    HasType Γ e (.poly T T2)
+    ∧ Subtyp Γ (T2.open_tvar T) U := by
+  generalize he1 : Exp.tapp e T = t0 at ht
+  induction ht <;> cases he1 <;> grind
+
+theorem HasType.tabs_inv
+  (ht : HasType Γ (.tabs T0 e) (.poly T1 U1)) :
+  ∃ U0,
+    HasType (Γ,X<:T0) e U0
+    ∧ Subtyp Γ T1 T0
+    ∧ Subtyp (Γ,X<:T1) U0 U1 := by
+  generalize he1 : Exp.tabs T0 e = t0 at ht
+  generalize he2 : Ty.poly T1 U1 = P at ht
+  induction ht <;> cases he1 <;> cases he2
+  case tabs T _ U h _ => use U; split_ands <;> grind
+  case sub ht ih hs =>
+    cases (Subtyp.poly_inv_right hs)
+    case inl h =>
+      have ⟨T2, U2, h⟩ := h
+      cases h; rename_i ih
+      have ⟨U0, ih1, ih2, ih3⟩ := ih rfl rfl
+      have ⟨h1, h2⟩ := Subtyp.poly_inv hs
+      use U0; split_ands <;> try grind
+      · have ih3' := ih3.retype (Retype.narrow_tvar h1)
+        grind [Ty.subst_id]
+    case inr h => grind [HasType.value_typing]
+
+theorem HasType.value_typing_arrow_inv
+  (hv : Exp.IsVal v) (ht : HasType Γ v (.arrow T U)) :
+  ∃ T0 e0, v = .abs T0 e0 := by
+  generalize he : Ty.arrow T U = P at ht
+  induction ht <;> try (solve | cases he | cases hv | aesop)
+  case sub ih =>
+    cases he; rename_i hs
+    cases (Subtyp.arrow_inv_right hs)
+    case inl h => aesop
+    case inr h => grind [HasType.value_typing]
+
+theorem HasType.value_typing_poly_inv
+  (hv : Exp.IsVal v) (ht : HasType Γ v (.poly T U)) :
+  ∃ T0 e0, v = .tabs T0 e0 := by
+  generalize he : Ty.poly T U = P at ht
+  induction ht <;> try (solve | cases he | cases hv | aesop)
+  case sub ih =>
+    cases he; rename_i hs
+    cases (Subtyp.poly_inv_right hs)
+    case inl h => aesop
+    case inr h => grind [HasType.value_typing]
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean
new file mode 100644
index 00000000..10ae07c7
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Preservation theorem for System F<:
+
+This module proves the preservation theorem for System F<:.
+Preservation states that if a well-typed expression takes a reduction step,
+the result is still well-typed with the same type.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Canonical
+
+/-- **Preservation theorem**: Well-typed expressions remain
+    well-typed after taking reduction steps.
+
+    If `∅ ⊢ e : T` and `e ⟶ e'`, then `∅ ⊢ e' : T`.
+
+    This is the fundamental type safety theorem establishing that computation
+    preserves typing invariants. Together with progress, this constitutes
+    the complete proof of type soundness for System F<:. -/
+theorem preservation
+  (ht : HasType .empty t T)
+  (hred : Reduce t t') :
+  HasType .empty t' T := by
+  induction hred generalizing T
+  case red_app_fun ih =>
+    have ⟨_, _, ht1, ht2, hs0⟩ := HasType.app_inv ht
+    apply HasType.sub hs0
+    apply HasType.app (ih ht1) ht2
+  case red_app_arg ih =>
+    have ⟨_, _, ht1, ht2, hs0⟩ := HasType.app_inv ht
+    apply HasType.sub hs0
+    apply HasType.app ht1 (ih ht2)
+  case red_app =>
+    have ⟨_, _, ht1, ht2, hs0⟩ := HasType.app_inv ht
+    have ⟨_, h1, h2, h3⟩  := HasType.abs_inv ht1
+    have ht2' := HasType.sub h2 ht2
+    have h1' := h1.retype (Retype.open_var ht2')
+    simp only [Ty.rename_succVar_open_var] at h1'
+    apply HasType.sub _ h1'
+    apply Subtyp.trans h3 hs0
+  case red_tapp_fun ih =>
+    have ⟨_, ht1, hs2⟩ := HasType.tapp_inv ht
+    apply HasType.sub hs2
+    apply HasType.tapp (ih ht1)
+  case red_tapp =>
+    have ⟨_, ht1, hs2⟩ := HasType.tapp_inv ht
+    have ⟨_, h1, h2, h3⟩ := HasType.tabs_inv ht1
+    have h1' := h1.retype (Retype.open_tvar h2)
+    have h3' := h3.retype (Retype.open_tvar Subtyp.refl)
+    apply HasType.sub _ h1'
+    apply Subtyp.trans h3' hs2
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean
new file mode 100644
index 00000000..20f4ded1
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Progress theorem for System F<:
+
+This module proves the progress theorem for System F<:.
+Progress states that well-typed expressions in the empty context are either values
+or can take a reduction step.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Canonical
+
+/-- Progress theorem: well-typed expressions in empty contexts either are values
+    or can take a reduction step. -/
+theorem progress
+  (ht : HasType Γ t T) (hem : Ctx.IsEmpty Γ) :
+  (∃ t', Reduce t t') ∨ t.IsVal := by
+  induction ht
+  case var hb => cases hem; cases hb
+  case sub ih => aesop
+  case abs => right; constructor
+  case tabs => right; constructor
+  case app ih1 ih2 =>
+    cases (ih1 hem)
+    case inl ih1 =>
+      have ⟨t1', ih1⟩ := ih1
+      left; constructor
+      apply Reduce.red_app_fun ih1
+    case inr ih1 =>
+      rename_i hvt _ _
+      have ⟨T0, e0, h⟩ := HasType.value_typing_arrow_inv ih1 hvt
+      cases h
+      left; constructor
+      apply Reduce.red_app
+  case tapp ih =>
+    specialize ih hem
+    cases ih
+    case inl ih =>
+      have ⟨t1', ih⟩ := ih
+      left; constructor
+      apply Reduce.red_tapp_fun ih
+    case inr ih =>
+      rename_i hvt
+      have := HasType.value_typing_poly_inv ih hvt
+      have ⟨T0, e0, h⟩ := this
+      cases h
+      left; constructor
+      apply Reduce.red_tapp
diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean
new file mode 100644
index 00000000..60a91853
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2025 Yichen Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yichen Xu.
+-/
+
+/-
+# Type system for System F<:
+
+This module defines the core type system for System F<: (System F with bounded quantification).
+
+The module defines:
+- `Subtyp`: The subtyping relation Γ ⊢ A <: B
+- `HasType`: The typing relation Γ ⊢ e : T
+
+System F<: extends System F with bounded type quantification.
+The subtyping relation includes structural rules (reflexivity, transitivity),
+the top type as universal supertype, contravariant function subtyping,
+and covariant bounded quantifier subtyping.
+
+The typing system is standard for System F<: with subsumption:
+if an expression has type A and A <: B, then the expression also has type B.
+-/
+
+import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax
+
+/-- The subtyping relation for System F<:. `Subtyp Γ A B` means that type `A` is a
+    subtype of type `B` under context `Γ`.
+
+    The rules include:
+    - `top`: Every type is a subtype of the top type
+    - `refl`: Subtyping is reflexive
+    - `trans`: Subtyping is transitive
+    - `tvar`: Type variables are subtypes of their bounds
+    - `arrow`: Function types are contravariant in domain, covariant in codomain
+    - `poly`: Polymorphic types are covariant in both bound and body -/
+@[grind]
+inductive Subtyp : Ctx s → Ty s → Ty s → Prop where
+/-- Every type is a subtype of the top type -/
+| top :
+  Subtyp Γ T .top
+/-- Subtyping is reflexive -/
+| refl :
+  Subtyp Γ T T
+/-- Subtyping is transitive -/
+| trans :
+  Subtyp Γ A B →
+  Subtyp Γ B C →
+  Subtyp Γ A C
+/-- Type variables are subtypes of their declared upper bounds -/
+| tvar :
+  Ctx.LookupTVar Γ X T →
+  Subtyp Γ (.tvar X) T
+/-- Function subtyping: contravariant in domain, covariant in codomain -/
+| arrow :
+  Subtyp Γ T2 T1 →
+  Subtyp Γ U1 U2 →
+  Subtyp Γ (.arrow T1 U1) (.arrow T2 U2)
+/-- Polymorphic subtyping: covariant in bound and body -/
+| poly :
+  Subtyp Γ T2 T1 →
+  Subtyp (Γ,X<:T2) U1 U2 →
+  Subtyp Γ (.poly T1 U1) (.poly T2 U2)
+
+/-- The typing relation for System F<:. `HasType Γ e T` means that expression `e`
+    has type `T` under context `Γ`.
+
+    The rules include:
+    - `var`: Type variables according to context lookup
+    - `sub`: Subsumption - if e : T₁ and T₁ <: T₂ then e : T₂
+    - `abs`: Function abstraction
+    - `tabs`: Type abstraction (polymorphic functions)
+    - `app`: Function application
+    - `tapp`: Type application (polymorphic instantiation) -/
+inductive HasType : Ctx s → Exp s → Ty s → Prop where
+/-- Term variables have the type assigned in the context -/
+| var :
+  Ctx.LookupVar Γ x T →
+  HasType Γ (.var x) T
+/-- Subsumption: if e : T₁ and T₁ <: T₂, then e : T₂ -/
+| sub :
+  Subtyp Γ T1 T2 →
+  HasType Γ t T1 →
+  HasType Γ t T2
+/-- Function abstraction: λx:T.e has type T → U if e has type U under x:T -/
+| abs :
+  HasType (Γ,x:T) t (U.rename Rename.succVar) →
+  HasType Γ (.abs T t) (.arrow T U)
+/-- Type abstraction: ΛX<:T.e has type ∀X<:T.U if e has type U under X<:T -/
+| tabs :
+  HasType (Γ,X<:T) t U →
+  HasType Γ (.tabs T t) (.poly T U)
+/-- Function application: if e₁ : T → U and e₂ : T, then e₁ e₂ : U -/
+| app :
+  HasType Γ t1 (.arrow T1 U1) →
+  HasType Γ t2 T1 →
+  HasType Γ (.app t1 t2) U1
+/-- Type application: if e : ∀X<:T.U and S <: T, then e[S] : U[X := S] -/
+| tapp :
+  HasType Γ t (.poly T U) →
+  HasType Γ (.tapp t T) (U.open_tvar T)