diff --git a/coq/_CoqProject b/coq/_CoqProject
index 45553df..a81a62d 100644
--- a/coq/_CoqProject
+++ b/coq/_CoqProject
@@ -8,6 +8,7 @@ Metatheory.v
 
 terms_debruijn.v
 equiv_debruijn.v
+subtype_debruijn.v
 subst_lemmas_debruijn.v
 
 terms.v
diff --git a/coq/subtype_debruijn.v b/coq/subtype_debruijn.v
new file mode 100644
index 0000000..4fe2ed0
--- /dev/null
+++ b/coq/subtype_debruijn.v
@@ -0,0 +1,46 @@
+(*
+ * This module defines the subtype relationship
+ *
+ * We distinguish between *representational* subtypes,
+ * where any high-level type is a subtype of its underlying
+ * representation type and *convertible* subtypes that
+ * are compatible at high level, but have a different representation
+ * that requires a conversion.
+ *)
+
+Require Import terms_debruijn.
+Require Import equiv_debruijn.
+
+(** Subtyping *)
+
+Create HintDb subtype_hints.
+
+Reserved Notation "s ':<=' t" (at level 50).
+Reserved Notation "s '~<=' t" (at level 50).
+
+(* Representational Subtype *)
+Inductive is_repr_subtype : type_DeBruijn -> type_DeBruijn -> Prop :=
+	| TSubRepr_Refl : forall t t', (t === t') -> (t :<= t')
+	| TSubRepr_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z)
+	| TSubRepr_Ladder : forall x' x y, (x :<= y) -> ([< x' ~ x >] :<= y)
+where "s ':<=' t" := (is_repr_subtype s t).
+
+(* Convertible Subtype *)
+Inductive is_conv_subtype : type_DeBruijn -> type_DeBruijn -> Prop :=
+	| TSubConv_Refl : forall t t', (t === t') -> (t ~<= t')
+	| TSubConv_Trans : forall x y z, (x ~<= y) -> (y ~<= z) -> (x ~<= z)
+	| TSubConv_Ladder : forall x' x y, (x ~<= y) -> ([< x' ~ x >] ~<= y)
+	| TSubConv_Morph : forall x y y', [< x ~ y >] ~<= [< x ~ y' >]
+where "s '~<=' t" := (is_conv_subtype s t).
+
+Hint Constructors is_repr_subtype :subtype_hints.
+Hint Constructors is_conv_subtype :subtype_hints.
+
+(* Every Representational Subtype is a Convertible Subtype *)
+
+Lemma syn_sub_is_sem_sub : forall x y, (x :<= y) -> (x ~<= y).
+Proof.
+	intros.
+	induction H.
+	all: eauto with subtype_hints.
+Qed.