diff --git a/coq/terms/debruijn.v b/coq/terms/debruijn.v
index f6e0505..9ecf6bc 100644
--- a/coq/terms/debruijn.v
+++ b/coq/terms/debruijn.v
@@ -187,6 +187,21 @@ Fixpoint expr_fv (e : expr_DeBruijn) {struct e} : atoms :=
   | ex_descend τ t' => (expr_fv t')
   end.
 
+(* get the list of all free type variables in an expression *)
+Fixpoint expr_fv_type (e : expr_DeBruijn) {struct e} : atoms :=
+  match e with
+  | ex_fvar n => {}
+  | ex_bvar y => {}
+  | ex_ty_abs t' => {}
+  | ex_ty_app t' σ => (expr_fv_type t') `union` (type_fv σ)
+  | ex_morph σ t' => (type_fv σ) `union` (expr_fv_type t')
+  | ex_abs σ t' => (type_fv σ) `union` (expr_fv_type t')
+  | ex_app t1 t2 => (expr_fv_type t1) `union` (expr_fv_type t2)
+  | ex_let t1 t2 => (expr_fv_type t1) `union` (expr_fv_type t2)
+  | ex_ascend τ t' => (expr_fv_type t')
+  | ex_descend τ t' => (expr_fv_type t')
+  end.
+
 (* substitute free variable x with expression s in t *)
 Fixpoint expr_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
   match t with