diff --git a/coq/equiv.v b/coq/equiv.v
index 9ad4a58..680fad3 100644
--- a/coq/equiv.v
+++ b/coq/equiv.v
@@ -43,7 +43,7 @@ Module Equiv.
 
 Reserved Notation "S '-->α' T" (at level 40).
 Inductive type_conv_alpha : type_term -> type_term -> Prop :=
-  | Eq_Alpha : forall x y t,
+  | TEq_Alpha : forall x y t,
   (type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
 where "S '-->α' T" := (type_conv_alpha S T).
 
@@ -171,23 +171,23 @@ Qed.
 
 Reserved Notation " S '===' T " (at level 40).
 Inductive type_eq : type_term -> type_term -> Prop :=
-  | L_Refl : forall x,
+  | TEq_Refl : forall x,
     x === x
 
-  | L_Trans : forall x y z,
+  | TEq_Trans : forall x y z,
     x === y ->
     y === z ->
     x === z
 
-  | L_Rename : forall x y,
+  | TEq_Rename : forall x y,
     x -->α y ->
     x === y
 
-  | L_Distribute : forall x y,
+  | TEq_Distribute : forall x y,
     x -->distribute-ladder y ->
     x === y
 
-  | L_Condense : forall x y,
+  | TEq_Condense : forall x y,
     x -->condense-ladder y ->
     x === y
 
@@ -203,27 +203,22 @@ Proof.
   intros.
   induction H.
   
-  1:{
-    apply L_Refl.
-  }
+  apply TEq_Refl.
 
-  3:{
-    apply L_Condense.
-    apply distribute_inverse.
-    apply H.
-  }
-  3:{
-    apply L_Distribute.
-    apply condense_inverse.
-    apply H.
-  }
-
-  apply L_Trans with (y:=y).
+  apply TEq_Trans with (y:=y).
   apply IHtype_eq2.
   apply IHtype_eq1.
 
   apply type_alpha_symm in H.
-  apply L_Rename.
+  apply TEq_Rename.
+  apply H.
+
+  apply TEq_Condense.
+  apply distribute_inverse.
+  apply H.
+
+  apply TEq_Distribute.
+  apply condense_inverse.
   apply H.
 Qed.
 
@@ -301,25 +296,26 @@ Proof.
   destruct t.
 
   exists type_unit.
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   
   exists (type_id s).
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   admit.
   
   exists (type_num n).
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   
   admit.
   
   exists (type_univ s t).
-  split. apply L_Refl.
+  split.
+  apply TEq_Refl.
   apply LNF.
   
 Admitted.
@@ -366,7 +362,7 @@ Example example_type_eq :
     (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
                (type_spec (type_id "Seq") (type_id "Byte"))).
 Proof.
-  apply L_Distribute.
+  apply TEq_Distribute.
   apply L_DistributeOverSpec2.
 Qed.