diff --git a/coq/bbencode.v b/coq/bbencode.v
index 36c0173..934d619 100644
--- a/coq/bbencode.v
+++ b/coq/bbencode.v
@@ -1,4 +1,5 @@
 From Coq Require Import Strings.String.
+
 Require Import terms.
 Require Import subst.
 Require Import smallstep.
@@ -7,35 +8,37 @@ Include Terms.
 Include Subst.
 Include Smallstep.
 
+Open Scope ladder_type_scope.
+Open Scope ladder_expr_scope.
 
 (*  let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
  *                ∀α.(α->α)->α->α
 *)
 Definition bb_zero : expr_term :=
   (expr_ty_abs "α"
-    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-      (expr_tm_abs "z" (type_var "α")
+    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_abs "z" (type_var "α")
         (expr_var "z")))).
 
 (*  let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
 *)
 Definition bb_one : expr_term :=
   (expr_ty_abs "α"
-    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-      (expr_tm_abs "z" (type_var "α")
-        (expr_tm_app (expr_var "s") (expr_var "z"))))).
+    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_abs "z" (type_var "α")
+        (expr_app (expr_var "s") (expr_var "z"))))).
 
 (*  let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
 *)
 Definition bb_two : expr_term :=
   (expr_ty_abs "α"
-    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-      (expr_tm_abs "z" (type_var "α")
-        (expr_tm_app (expr_var "s") (expr_tm_app (expr_var "s") (expr_var "z")))))).
+    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_abs "z" (type_var "α")
+        (expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).
 
 
 Definition bb_succ : expr_term :=
-  (expr_tm_abs "n" (type_ladder (type_id "ℕ")
+  (expr_abs "n" (type_ladder (type_id "ℕ")
                     (type_ladder (type_id "BBNat")
                      (type_univ "α"
                       (type_fun (type_fun (type_var "α") (type_var "α"))
@@ -43,10 +46,10 @@ Definition bb_succ : expr_term :=
 
        (expr_ascend (type_ladder (type_id "ℕ") (type_id "BBNat"))
           (expr_ty_abs "α"
-            (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-              (expr_tm_abs "z" (type_var "α")
-                (expr_tm_app (expr_var "s")
-                  (expr_tm_app (expr_tm_app
+            (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+              (expr_abs "z" (type_var "α")
+                (expr_app (expr_var "s")
+                  (expr_app (expr_app
                       (expr_ty_app (expr_var "n") (type_var "α"))
                       (expr_var "s"))
                     (expr_var "z")))))))).
@@ -58,25 +61,25 @@ Definition e1 : expr_term :=
                             (type_fun (type_fun (type_var "α") (type_var "α"))
                               (type_fun (type_var "α") (type_var "α"))))))
                        bb_zero
-                       (expr_tm_app (expr_tm_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
+                       (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
   ).
 
-Definition t1 : expr_term := (expr_tm_app (expr_var "x") (expr_var "x")).
+Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).
 
 Compute (expr_subst "x"
-    (expr_ty_abs "α" (expr_tm_abs "a" (type_var "α") (expr_var "a")))
+    (expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
     bb_one
 ).
 
 Example  example_let_reduction :
-    e1 -->β  (expr_tm_app (expr_tm_app (expr_var "+") bb_zero) bb_zero).
+    e1 -->β  (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
 Proof.
     apply E_AppLet.
 Qed.
 
-Compute     (expr_tm_app bb_succ bb_zero) -->β bb_one.
+Compute     (expr_app bb_succ bb_zero) -->β bb_one.
 
 Example  example_succ :
-    (expr_tm_app bb_succ bb_zero) -->β bb_one.
+    (expr_app bb_succ bb_zero) -->β bb_one.
 Proof.
 Admitted.
diff --git a/coq/smallstep.v b/coq/smallstep.v
index c3da0a3..45fee88 100644
--- a/coq/smallstep.v
+++ b/coq/smallstep.v
@@ -16,11 +16,11 @@ Reserved Notation " s '-->eval' t " (at level 40).
 Inductive beta_step : expr_term -> expr_term -> Prop :=
   | E_App1 : forall e1 e1' e2,
     e1 -->β e1' ->
-    (expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
+    (expr_app e1 e2) -->β (expr_app e1' e2)
 
   | E_App2 : forall e1 e2 e2',
     e2 -->β e2' ->
-    (expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
+    (expr_app e1 e2) -->β (expr_app e1 e2')
 
   | E_TypApp : forall e e' τ,
     e -->β e' ->
diff --git a/coq/subst.v b/coq/subst.v
index e36e000..3ad385d 100644
--- a/coq/subst.v
+++ b/coq/subst.v
@@ -112,9 +112,9 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
   | expr_var name => if (eqb v name) then n else e0
   | expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
   | expr_ty_app e t => expr_ty_app (expr_subst v n e) t
-  | expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs x t (expr_subst v n e)
-  | expr_tm_abs_morph x t e => if (eqb v x) then e0 else expr_tm_abs_morph x t (expr_subst v n e)
-  | expr_tm_app e a => expr_tm_app (expr_subst v n e) (expr_subst v n a)
+  | expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
+  | expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e)
+  | expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
   | expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
   | expr_ascend t e => expr_ascend t (expr_subst v n e)
   | expr_descend t e => expr_descend t (expr_subst v n e)
diff --git a/coq/terms.v b/coq/terms.v
index 21ff0d1..6bdada5 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -22,9 +22,9 @@ Inductive expr_term : Type :=
   | expr_var : string -> expr_term
   | expr_ty_abs : string -> expr_term -> expr_term
   | expr_ty_app : expr_term -> type_term -> expr_term
-  | expr_tm_abs : string -> type_term -> expr_term -> expr_term
-  | expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
-  | expr_tm_app : expr_term -> expr_term -> expr_term
+  | expr_abs   : string -> type_term -> expr_term -> expr_term
+  | expr_morph : string -> type_term -> expr_term -> expr_term
+  | expr_app : expr_term -> expr_term -> expr_term
   | expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
   | expr_ascend : type_term -> expr_term -> expr_term
   | expr_descend : type_term -> expr_term -> expr_term
@@ -32,8 +32,8 @@ Inductive expr_term : Type :=
 
 (* values *)
 Inductive is_value : expr_term -> Prop :=
-  | V_ValAbs : forall x τ e,
-    (is_value (expr_tm_abs x τ e))
+  | V_Abs : forall x τ e,
+    (is_value (expr_abs x τ e))
 
   | V_TypAbs : forall τ e,
     (is_value (expr_ty_abs τ e))
@@ -43,6 +43,8 @@ Inductive is_value : expr_term -> Prop :=
     (is_value (expr_ascend τ e))
 .
 
+
+
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.
@@ -71,10 +73,14 @@ Notation "[[ e ]]" := e
   (e custom ladder_expr at level 80) : ladder_expr_scope.
 Notation "'%' x '%'" := (expr_var x%string)
   (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
-Notation "'λ' x τ '↦' e" := (expr_tm_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
+Notation "'λ' x τ '↦' e" := (expr_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
 Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
   (in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
 
+
+
+(* EXAMPLES *)
+
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 
diff --git a/coq/typing.v b/coq/typing.v
index 316a27d..50af8b4 100644
--- a/coq/typing.v
+++ b/coq/typing.v
@@ -52,12 +52,12 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
   | T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
     (context_contains Γ x σ) ->
     Γ |- t \is τ ->
-    Γ |- (expr_tm_abs x σ t) \is (type_fun σ τ)
+    Γ |- (expr_abs x σ t) \is (type_fun σ τ)
 
   | T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
     Γ |- f \is (type_fun σ τ) ->
     Γ |- a \is σ ->
-    Γ |- (expr_tm_app f a) \is τ
+    Γ |- (expr_app f a) \is τ
 
   | T_Sub : forall Γ x τ τ',
     Γ |- x \is τ ->
@@ -88,17 +88,17 @@ Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
   | T_CompatMorphAbs : forall Γ x t τ τ',
     Γ |- t \compatible τ ->
     (τ ~<= τ') ->
-    Γ |- (expr_tm_abs_morph x τ t) \compatible (type_morph τ τ')
+    Γ |- (expr_morph x τ t) \compatible (type_morph τ τ')
 
   | T_CompatAbs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
     (context_contains Γ x σ) ->
     Γ |- t \compatible τ ->
-    Γ |- (expr_tm_abs x σ t) \compatible (type_fun σ τ)
+    Γ |- (expr_abs x σ t) \compatible (type_fun σ τ)
 
   | T_CompatApp : forall Γ f a σ τ,
     (Γ |- f \compatible (type_fun σ τ)) ->
     (Γ |- a \compatible σ) ->
-    (Γ |- (expr_tm_app f a) \compatible τ)
+    (Γ |- (expr_app f a) \compatible τ)
 
   | T_CompatImplicitCast : forall Γ h x τ τ',
     (context_contains Γ h (type_morph τ τ')) ->
@@ -112,10 +112,13 @@ Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
 
 where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
 
+Definition is_well_typed (e:expr_term) : Prop :=
+  exists Γ τ,
+  Γ |- e \compatible τ
+.
 
 (* Examples *)
 
-
 Example typing1 :
   forall Γ,
   (context_contains Γ "x" [ %"T"% ]) ->