diff --git a/coq/typing/morph.v b/coq/typing/morph.v
index 4ec518d..9534049 100644
--- a/coq/typing/morph.v
+++ b/coq/typing/morph.v
@@ -6,6 +6,7 @@ Require Import Atom.
 Import AtomImpl.
 From Coq Require Import Lists.List.
 Import ListNotations.
+Require Import Environment.
 
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
@@ -19,7 +20,7 @@ Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop :=
     (Γ |- τ ~~> τ')
 
   | M_Single : forall Γ h τ τ',
-    In (h, [< τ ->morph τ' >]) Γ ->
+    (binds h [< τ ->morph τ' >] Γ) ->
     (Γ |- τ ~~> τ')
 
   | M_Chain : forall Γ τ τ' τ'',
@@ -63,7 +64,7 @@ Inductive translate_morphism_path : env -> type_DeBruijn -> type_DeBruijn -> exp
       [{ λ (σ ~ τ) ↦morph (m (%0 des τ)) as σ }])
 
   | Translate_Single : forall Γ h τ τ',
-    In (h, [< τ ->morph τ' >]) Γ ->
+    binds h [< τ ->morph τ' >] Γ ->
     (Γ |- [[ τ ~~> τ' ]] = [{ $h }])
 
   | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
diff --git a/coq/typing/typing.v b/coq/typing/typing.v
index b61762b..6decf89 100644
--- a/coq/typing/typing.v
+++ b/coq/typing/typing.v
@@ -13,7 +13,7 @@ Open Scope ladder_expr_scope.
 Reserved Notation "Γ '|-' x '\is' X"  (at level 101).
 Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop :=
   | T_Var : forall Γ x τ,
-    (In (x, τ) Γ) ->
+    (binds x τ Γ) ->
     (Γ |- [{ $x }] \is τ)
 
   | T_Let : forall Γ L s σ t τ,
@@ -79,7 +79,7 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru
   | Expand_Let : forall Γ L e e' t t' σ τ,
     (Γ |- e \is σ) ->
     (forall x : atom, x `notin` L ->
-      ( (x,σ)::Γ |- (expr_open t (ex_fvar x)) \is τ) ->
+      ( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ) ->
       ( (x,σ)::Γ |- [[ t \is τ ]] = t' )
     ) ->
     (Γ |- [[ e \is σ ]] = e') ->