diff --git a/coq/_CoqProject b/coq/_CoqProject
index 4be14fa..417f869 100644
--- a/coq/_CoqProject
+++ b/coq/_CoqProject
@@ -10,7 +10,7 @@ metatheory/Metatheory.v
 terms/debruijn.v
 terms/equiv.v
 terms/eval.v
-typing/context.v
+typing/env.v
 typing/subtype.v
 typing/morph.v
 typing/typing.v
diff --git a/coq/terms/eval.v b/coq/terms/eval.v
index a1ae5ea..506b32c 100644
--- a/coq/terms/eval.v
+++ b/coq/terms/eval.v
@@ -3,7 +3,6 @@ Import ListNotations.
 Require Import Atom.
 Require Import debruijn.
 Require Import subtype.
-Require Import context.
 Require Import morph.
 Require Import typing.
 
diff --git a/coq/typing/context.v b/coq/typing/context.v
deleted file mode 100644
index 595fa12..0000000
--- a/coq/typing/context.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Atom.
-Require Import debruijn.
-
-Definition context : Type := (list (atom * type_DeBruijn)).
diff --git a/coq/typing/env.v b/coq/typing/env.v
new file mode 100644
index 0000000..d4c0719
--- /dev/null
+++ b/coq/typing/env.v
@@ -0,0 +1,5 @@
+Require Import Atom.
+Require Import Environment.
+Require Import debruijn.
+
+Notation env := (list (atom * type_DeBruijn)).
diff --git a/coq/typing/morph.v b/coq/typing/morph.v
index b94619a..4ec518d 100644
--- a/coq/typing/morph.v
+++ b/coq/typing/morph.v
@@ -1,7 +1,7 @@
 Require Import debruijn.
 Require Import equiv.
 Require Import subtype.
-Require Import context.
+Require Import env.
 Require Import Atom.
 Import AtomImpl.
 From Coq Require Import Lists.List.
@@ -13,7 +13,7 @@ Open Scope ladder_expr_scope.
 (* Given a context, there is a morphism path from τ to τ' *)
 Reserved Notation "Γ '|-' σ '~~>' τ" (at level 101).
 
-Inductive morphism_path : context -> type_DeBruijn -> type_DeBruijn -> Prop :=
+Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop :=
   | M_Sub : forall Γ τ τ',
     τ :<= τ' ->
     (Γ |- τ ~~> τ')
@@ -51,7 +51,7 @@ Reserved Notation "Γ '|-' '[[' σ '~~>' τ ']]' '=' m" (at level 101).
 (* some atom for the 'map' function on lists *)
 Parameter at_map : atom.
 
-Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
+Inductive translate_morphism_path : env -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
   | Translate_Descend : forall Γ τ τ',
     (τ :<= τ') ->
     (Γ |- [[ τ ~~> τ' ]] = [{ λ τ ↦morph (%0 des τ') }])
diff --git a/coq/typing/typing.v b/coq/typing/typing.v
index 474028c..b61762b 100644
--- a/coq/typing/typing.v
+++ b/coq/typing/typing.v
@@ -4,14 +4,14 @@ Require Import Metatheory.
 Require Import Atom.
 Require Import debruijn.
 Require Import subtype.
-Require Import context.
+Require Import env.
 Require Import morph.
 
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 
 Reserved Notation "Γ '|-' x '\is' X"  (at level 101).
-Inductive typing : context -> expr_DeBruijn -> type_DeBruijn -> Prop :=
+Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop :=
   | T_Var : forall Γ x τ,
     (In (x, τ) Γ) ->
     (Γ |- [{ $x }] \is τ)
@@ -70,7 +70,7 @@ where "Γ '|-' x '\is' τ" := (typing Γ x τ).
 
 Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f"  (at level 101).
 
-Inductive translate_typing : context -> expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
+Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
 
   | Expand_Var : forall Γ x τ,
     (Γ |- [{ $x }] \is τ) ->