diff --git a/EvaluationContexts.v b/EvaluationContexts.v
index a5b0c13..94f5d93 100644
--- a/EvaluationContexts.v
+++ b/EvaluationContexts.v
@@ -91,25 +91,25 @@ Module Stlc.
   | Nat                  (* Numbers *)
   | Fun (dom ran : type) (* Functions *).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2.
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2.
 
-  Local Hint Constructors value plug step0 step hasty : core.
+  Local Hint Constructors value plug step0 step has_ty : core.
 
   (** * Now we adapt the automated proof of type soundness. *)
 
@@ -121,15 +121,15 @@ Module Stlc.
 
              | [ H : step _ _ |- _ ] => invert H
              | [ H : step0 _ _ |- _ ] => invert1 H
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
-             | [ H : hasty _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
+             | [ H : has_ty _ _ _ |- _ ] => invert1 H
              | [ H : plug _ _ _ |- _ ] => invert1 H
              end; subst.
 
   Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
 
   Lemma progress : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> value e
     \/ (exists e' : exp, step e e').
   Proof.
@@ -148,9 +148,9 @@ Module Stlc.
   Local Hint Resolve weakening_override : core.
 
   Lemma weakening : forall G e t,
-    hasty G e t
+    has_ty G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     induct 1; t.
   Qed.
@@ -159,20 +159,20 @@ Module Stlc.
 
   (* Replacing a typing context with an equal one has no effect (useful to guide
    * proof search as a hint). *)
-  Lemma hasty_change : forall G e t,
-    hasty G e t
+  Lemma has_ty_change : forall G e t,
+    has_ty G e t
     -> forall G', G' = G
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution : forall G x t' e t e',
-    hasty (G $+ (x, t')) e t
-    -> hasty $0 e' t'
-    -> hasty G (subst e' x e) t.
+    has_ty (G $+ (x, t')) e t
+    -> has_ty $0 e' t'
+    -> has_ty G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -181,8 +181,8 @@ Module Stlc.
 
   Lemma preservation0 : forall e1 e2,
     step0 e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
@@ -193,8 +193,8 @@ Module Stlc.
       plug C e1 e1'
       -> forall e2 e2' t, plug C e2 e2'
       -> step0 e1 e2
-      -> hasty $0 e1' t
-      -> hasty $0 e2' t.
+      -> has_ty $0 e1' t
+      -> has_ty $0 e2' t.
   Proof.
     induct 1; t.
   Qed.
@@ -203,21 +203,21 @@ Module Stlc.
   
   Lemma preservation : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
 
   Local Hint Resolve progress preservation : core.
 
-  Theorem safety : forall e t, hasty $0 e t
+  Theorem safety : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e)
                     (fun e' => value e'
                                \/ exists e'', step e' e'').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
 
@@ -414,35 +414,35 @@ Module StlcPairs.
   | Fun (dom ran : type)
   | Prod (t1 t2 : type) (* "Prod" for "product," as in Cartesian product *).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty G e1 t1
-    -> hasty G e2 t2
-    -> hasty G (Pair e1 e2) (Prod t1 t2)
+    has_ty G e1 t1
+    -> has_ty G e2 t2
+    -> has_ty G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Fst e1) t1
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Snd e1) t2.
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Snd e1) t2.
 
-  Local Hint Constructors value plug step0 step hasty : core.
+  Local Hint Constructors value plug step0 step has_ty : core.
 
   Ltac t0 := match goal with
              | [ H : ex _ |- _ ] => invert H
@@ -452,18 +452,18 @@ Module StlcPairs.
 
              | [ H : step _ _ |- _ ] => invert H
              | [ H : step0 _ _ |- _ ] => invert1 H
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
                (* Change here!  We need to enforce there is at most one
                 * remaining subgoal, or we'll keep doing useless [value]
                 * inversions ad infinitum. *)
-             | [ H : hasty _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ _ _ |- _ ] => invert1 H
              | [ H : plug _ _ _ |- _ ] => invert1 H
              end; subst.
 
   Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
 
   Lemma progress : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> value e
     \/ (exists e' : exp, step e e').
   Proof.
@@ -482,9 +482,9 @@ Module StlcPairs.
   Local Hint Resolve weakening_override : core.
 
   Lemma weakening : forall G e t,
-    hasty G e t
+    has_ty G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     induct 1; t.
   Qed.
@@ -493,20 +493,20 @@ Module StlcPairs.
 
   (* Replacing a typing context with an equal one has no effect (useful to guide
    * proof search as a hint). *)
-  Lemma hasty_change : forall G e t,
-    hasty G e t
+  Lemma has_ty_change : forall G e t,
+    has_ty G e t
     -> forall G', G' = G
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution : forall G x t' e t e',
-    hasty (G $+ (x, t')) e t
-    -> hasty $0 e' t'
-    -> hasty G (subst e' x e) t.
+    has_ty (G $+ (x, t')) e t
+    -> has_ty $0 e' t'
+    -> has_ty G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -515,8 +515,8 @@ Module StlcPairs.
 
   Lemma preservation0 : forall e1 e2,
     step0 e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
@@ -527,8 +527,8 @@ Module StlcPairs.
       plug C e1 e1'
       -> forall e2 e2' t, plug C e2 e2'
       -> step0 e1 e2
-      -> hasty $0 e1' t
-      -> hasty $0 e2' t.
+      -> has_ty $0 e1' t
+      -> has_ty $0 e2' t.
   Proof.
     induct 1; t.
   Qed.
@@ -537,21 +537,21 @@ Module StlcPairs.
   
   Lemma preservation : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
 
   Local Hint Resolve progress preservation : core.
 
-  Theorem safety : forall e t, hasty $0 e t
+  Theorem safety : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e)
                     (fun e' => value e'
                                \/ exists e'', step e' e'').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
 End StlcPairs.
@@ -703,48 +703,48 @@ Module StlcSums.
   (* New case: *)
   | Sum (t1 t2 : type).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty G e1 t1
-    -> hasty G e2 t2
-    -> hasty G (Pair e1 e2) (Prod t1 t2)
+    has_ty G e1 t1
+    -> has_ty G e2 t2
+    -> has_ty G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Fst e1) t1
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Snd e1) t2
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Snd e1) t2
 
   (* New cases: *)
   | HtInl : forall G e1 t1 t2,
-      hasty G e1 t1
-      -> hasty G (Inl e1) (Sum t1 t2)
+      has_ty G e1 t1
+      -> has_ty G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty G e1 t2
-      -> hasty G (Inr e1) (Sum t1 t2)
+      has_ty G e1 t2
+      -> has_ty G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty G e (Sum t1 t2)
-      -> hasty (G $+ (x1, t1)) e1 t
-      -> hasty (G $+ (x2, t2)) e2 t
-      -> hasty G (Match e x1 e1 x2 e2) t.
+      has_ty G e (Sum t1 t2)
+      -> has_ty (G $+ (x1, t1)) e1 t
+      -> has_ty (G $+ (x2, t2)) e2 t
+      -> has_ty G (Match e x1 e1 x2 e2) t.
 
-  Local Hint Constructors value plug step0 step hasty : core.
+  Local Hint Constructors value plug step0 step has_ty : core.
 
   Ltac t0 := match goal with
              | [ H : ex _ |- _ ] => invert H
@@ -754,13 +754,13 @@ Module StlcSums.
 
              | [ H : step _ _ |- _ ] => invert H
              | [ H : step0 _ _ |- _ ] => invert1 H
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
 
              (* New case!  For sums, we sometimes need to consider two rules for
               * one [value] inversion. *)
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
 
-             | [ H : hasty _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ _ _ |- _ ] => invert1 H
              | [ H : plug _ _ _ |- _ ] => invert1 H
              end; subst.
 
@@ -768,7 +768,7 @@ Module StlcSums.
                                                                  (* change! --^ *)
 
   Lemma progress : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> value e
     \/ (exists e' : exp, step e e').
   Proof.
@@ -787,9 +787,9 @@ Module StlcSums.
   Local Hint Resolve weakening_override : core.
 
   Lemma weakening : forall G e t,
-    hasty G e t
+    has_ty G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     induct 1; t.
   Qed.
@@ -798,20 +798,20 @@ Module StlcSums.
 
   (* Replacing a typing context with an equal one has no effect (useful to guide
    * proof search as a hint). *)
-  Lemma hasty_change : forall G e t,
-    hasty G e t
+  Lemma has_ty_change : forall G e t,
+    has_ty G e t
     -> forall G', G' = G
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution : forall G x t' e t e',
-    hasty (G $+ (x, t')) e t
-    -> hasty $0 e' t'
-    -> hasty G (subst e' x e) t.
+    has_ty (G $+ (x, t')) e t
+    -> has_ty $0 e' t'
+    -> has_ty G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -820,8 +820,8 @@ Module StlcSums.
 
   Lemma preservation0 : forall e1 e2,
     step0 e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
@@ -832,8 +832,8 @@ Module StlcSums.
       plug C e1 e1'
       -> forall e2 e2' t, plug C e2 e2'
       -> step0 e1 e2
-      -> hasty $0 e1' t
-      -> hasty $0 e2' t.
+      -> has_ty $0 e1' t
+      -> has_ty $0 e2' t.
   Proof.
     induct 1; t.
   Qed.
@@ -842,21 +842,21 @@ Module StlcSums.
   
   Lemma preservation : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
 
   Local Hint Resolve progress preservation : core.
 
-  Theorem safety : forall e t, hasty $0 e t
+  Theorem safety : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e)
                     (fun e' => value e'
                                \/ exists e'', step e' e'').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
 End StlcSums.
@@ -1031,55 +1031,55 @@ Module StlcExceptions.
   | Prod (t1 t2 : type)
   | Sum (t1 t2 : type).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty G e1 t1
-    -> hasty G e2 t2
-    -> hasty G (Pair e1 e2) (Prod t1 t2)
+    has_ty G e1 t1
+    -> has_ty G e2 t2
+    -> has_ty G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Fst e1) t1
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Snd e1) t2
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Snd e1) t2
   | HtInl : forall G e1 t1 t2,
-      hasty G e1 t1
-      -> hasty G (Inl e1) (Sum t1 t2)
+      has_ty G e1 t1
+      -> has_ty G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty G e1 t2
-      -> hasty G (Inr e1) (Sum t1 t2)
+      has_ty G e1 t2
+      -> has_ty G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty G e (Sum t1 t2)
-      -> hasty (G $+ (x1, t1)) e1 t
-      -> hasty (G $+ (x2, t2)) e2 t
-      -> hasty G (Match e x1 e1 x2 e2) t
+      has_ty G e (Sum t1 t2)
+      -> has_ty (G $+ (x1, t1)) e1 t
+      -> has_ty (G $+ (x2, t2)) e2 t
+      -> has_ty G (Match e x1 e1 x2 e2) t
 
   (* New cases: *)
   | HtThrow : forall G e1 t,
-      hasty G e1 Nat
-      -> hasty G (Throw e1) t
+      has_ty G e1 Nat
+      -> has_ty G (Throw e1) t
   | HtCatch : forall G e x1 e1 t,
-      hasty G e t
-      -> hasty (G $+ (x1, Nat)) e1 t
-      -> hasty G (Catch e x1 e1) t.
+      has_ty G e t
+      -> has_ty (G $+ (x1, Nat)) e1 t
+      -> has_ty G (Catch e x1 e1) t.
 
-  Local Hint Constructors value plug step0 step hasty : core.
+  Local Hint Constructors value plug step0 step has_ty : core.
 
   Ltac t0 := match goal with
              | [ H : ex _ |- _ ] => invert H
@@ -1089,11 +1089,11 @@ Module StlcExceptions.
 
              | [ H : step _ _ |- _ ] => invert H
              | [ H : step0 _ _ |- _ ] => invert1 H
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
 
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
 
-             | [ H : hasty _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ _ _ |- _ ] => invert1 H
              | [ H : plug _ _ _ _ |- _ ] => invert1 H (* added an underscore *)
              end; subst.
 
@@ -1102,7 +1102,7 @@ Module StlcExceptions.
   Local Hint Extern 1 (_ <> Hole) => equality : core.
 
   Lemma progress : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> value e
     \/ (exists n : nat, e = Throw (Const n))
     \/ (exists e' : exp, step e e').
@@ -1122,9 +1122,9 @@ Module StlcExceptions.
   Local Hint Resolve weakening_override : core.
 
   Lemma weakening : forall G e t,
-    hasty G e t
+    has_ty G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     induct 1; t.
   Qed.
@@ -1133,20 +1133,20 @@ Module StlcExceptions.
 
   (* Replacing a typing context with an equal one has no effect (useful to guide
    * proof search as a hint). *)
-  Lemma hasty_change : forall G e t,
-    hasty G e t
+  Lemma has_ty_change : forall G e t,
+    has_ty G e t
     -> forall G', G' = G
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution : forall G x t' e t e',
-    hasty (G $+ (x, t')) e t
-    -> hasty $0 e' t'
-    -> hasty G (subst e' x e) t.
+    has_ty (G $+ (x, t')) e t
+    -> has_ty $0 e' t'
+    -> has_ty G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -1155,8 +1155,8 @@ Module StlcExceptions.
 
   Lemma throw_well_typed : forall C v e,
       plug false C (Throw v) e
-      -> forall t, hasty $0 e t
-      -> hasty $0 v Nat.
+      -> forall t, has_ty $0 e t
+      -> has_ty $0 v Nat.
   Proof.
     induct 1; invert 1; t.
   Qed.
@@ -1165,8 +1165,8 @@ Module StlcExceptions.
     
   Lemma preservation0 : forall e1 e2,
     step0 e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
@@ -1177,8 +1177,8 @@ Module StlcExceptions.
       plug true C e1 e1'
       -> forall e2 e2' t, plug true C e2 e2'
       -> step0 e1 e2
-      -> hasty $0 e1' t
-      -> hasty $0 e2' t.
+      -> has_ty $0 e1' t
+      -> has_ty $0 e2' t.
   Proof.
     induct 1; t.
   Qed.
@@ -1187,22 +1187,22 @@ Module StlcExceptions.
   
   Lemma preservation : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
 
   Local Hint Resolve progress preservation : core.
 
-  Theorem safety : forall e t, hasty $0 e t
+  Theorem safety : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e)
                     (fun e' => value e'
                                \/ (exists n, e' = Throw (Const n))
                                \/ exists e'', step e' e'').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
 End StlcExceptions.
@@ -1316,7 +1316,7 @@ Module StlcMutable.
     plug C e e'
     -> plug (Match1 C x1 e1 x2 e2) e (Match e' x1 e1 x2 e2)
   
-   (* Our new plugging rules *)            
+  (* Our new plugging rules *)            
   | PluSetVar1 : forall x e e' C,
       plug C e e'
       -> plug (SetVar1 x C) e (SetVar x e').
@@ -1378,62 +1378,62 @@ Module StlcMutable.
 
   (* Now there will be two typing contexts, one for mutable variables and one
    * for immutable. *)
-  Inductive hasty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty M G (Var x) t
+    -> has_ty M G (Var x) t
   | HtConst : forall G n,
-    hasty M G (Const n) Nat
+    has_ty M G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty M G e1 Nat
-    -> hasty M G e2 Nat
-    -> hasty M G (Plus e1 e2) Nat
+    has_ty M G e1 Nat
+    -> has_ty M G e2 Nat
+    -> has_ty M G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty M (G $+ (x, t1)) e1 t2
-    -> hasty M G (Abs x e1) (Fun t1 t2)
+    has_ty M (G $+ (x, t1)) e1 t2
+    -> has_ty M G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty M G e1 (Fun t1 t2)
-    -> hasty M G e2 t1
-    -> hasty M G (App e1 e2) t2
+    has_ty M G e1 (Fun t1 t2)
+    -> has_ty M G e2 t1
+    -> has_ty M G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty M G e1 t1
-    -> hasty M G e2 t2
-    -> hasty M G (Pair e1 e2) (Prod t1 t2)
+    has_ty M G e1 t1
+    -> has_ty M G e2 t2
+    -> has_ty M G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Fst e1) t1
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Snd e1) t2
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Snd e1) t2
   | HtInl : forall G e1 t1 t2,
-      hasty M G e1 t1
-      -> hasty M G (Inl e1) (Sum t1 t2)
+      has_ty M G e1 t1
+      -> has_ty M G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty M G e1 t2
-      -> hasty M G (Inr e1) (Sum t1 t2)
+      has_ty M G e1 t2
+      -> has_ty M G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty M G e (Sum t1 t2)
-      -> hasty M (G $+ (x1, t1)) e1 t
-      -> hasty M (G $+ (x2, t2)) e2 t
-      -> hasty M G (Match e x1 e1 x2 e2) t
+      has_ty M G e (Sum t1 t2)
+      -> has_ty M (G $+ (x1, t1)) e1 t
+      -> has_ty M (G $+ (x2, t2)) e2 t
+      -> has_ty M G (Match e x1 e1 x2 e2) t
 
   (* New cases: *)
   | HtGetVar : forall G x t,
       M $? x = Some t
-      -> hasty M G (GetVar x) t
+      -> has_ty M G (GetVar x) t
   | HtSetVar : forall G x e t,
       M $? x = Some t
-      -> hasty M G e t
-      -> hasty M G (SetVar x e) t.
+      -> has_ty M G e t
+      -> has_ty M G (SetVar x e) t.
                
-  Local Hint Constructors value plug step0 step1 step hasty : core.
+  Local Hint Constructors value plug step0 step1 step has_ty : core.
 
   (* Let's characterize what makes a typing context and a variable valuation
    * compatible. *)
   Definition compatible (M : fmap var type) (env : valuation) :=
     forall x t, M $? x = Some t
                 -> exists v, env $? x = Some v
-                             /\ hasty M $0 v t.
+                             /\ has_ty M $0 v t.
   
   Ltac t0 := match goal with
              | [ H : ex _ |- _ ] => invert H
@@ -1443,11 +1443,11 @@ Module StlcMutable.
 
              | [ H : step _ _ |- _ ] => invert H
              | [ H : step0 _ _ |- _ ] => invert1 H
-             (* Add a few extra underscores below, for new [hasty] argument. *)
-             | [ H : hasty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
-             | [ H : hasty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
+             (* Add a few extra underscores below, for new [has_ty] argument. *)
+             | [ H : has_ty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
+             | [ H : has_ty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
 
-             | [ H : hasty _ _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ _ _ _ |- _ ] => invert1 H
              | [ H : plug _ _ _ |- _ ] => invert1 H
 
              (* New cases: *)
@@ -1461,7 +1461,7 @@ Module StlcMutable.
   Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 7.
   
   Lemma progress : forall M e t,
-    hasty M $0 e t
+    has_ty M $0 e t
     -> forall env, compatible M env
     -> value e
     \/ exists st', step (env, e) st'.
@@ -1480,29 +1480,29 @@ Module StlcMutable.
 
   Local Hint Resolve weakening_override : core.
 
-  Lemma weakening : forall M G e t, hasty M G e t
+  Lemma weakening : forall M G e t, has_ty M G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty M G' e t.
+      -> has_ty M G' e t.
   Proof.
     induct 1; t.
   Qed.
 
   Local Hint Resolve weakening : core.
 
-  Lemma hasty_change : forall M G e t,
-    hasty M G e t
+  Lemma has_ty_change : forall M G e t,
+    has_ty M G e t
     -> forall G', G' = G
-      -> hasty M G' e t.
+      -> has_ty M G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution : forall M G x t' e t e',
-    hasty M (G $+ (x, t')) e t
-    -> hasty M $0 e' t'
-    -> hasty M G (subst e' x e) t.
+    has_ty M (G $+ (x, t')) e t
+    -> has_ty M $0 e' t'
+    -> has_ty M G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -1512,7 +1512,7 @@ Module StlcMutable.
   Lemma compatible_bind : forall M env x v t,
       compatible M env
       -> M $? x = Some t
-      -> hasty M $0 v t
+      -> has_ty M $0 v t
       -> compatible M (env $+ (x, v)).
   Proof.
     unfold compatible; first_order.
@@ -1525,11 +1525,11 @@ Module StlcMutable.
 
   Local Hint Resolve compatible_bind : core.
 
-  Lemma compatible_hasty : forall M env x v t,
+  Lemma compatible_has_ty : forall M env x v t,
       compatible M env
       -> env $? x = Some v
       -> M $? x = Some t
-      -> hasty M $0 v t.
+      -> has_ty M $0 v t.
   Proof.
     t.
     specialize (H _ _ H1); first_order.
@@ -1538,12 +1538,12 @@ Module StlcMutable.
     assumption.
   Qed.
 
-  Local Hint Immediate compatible_hasty : core.
+  Local Hint Immediate compatible_has_ty : core.
 
   Lemma preservation0 : forall M e1 e2,
     step0 e1 e2
-    -> forall t, hasty M $0 e1 t
-      -> hasty M $0 e2 t.
+    -> forall t, has_ty M $0 e1 t
+      -> has_ty M $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
@@ -1552,16 +1552,16 @@ Module StlcMutable.
   
   Lemma preservation1_exp : forall M env1 e1 env2 e2,
     step1 (env1, e1) (env2, e2)
-    -> forall t, hasty M $0 e1 t
+    -> forall t, has_ty M $0 e1 t
       -> compatible M env1
-      -> hasty M $0 e2 t.
+      -> has_ty M $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
 
   Lemma preservation1_env : forall M env1 e1 env2 e2,
     step1 (env1, e1) (env2, e2)
-    -> forall t, hasty M $0 e1 t
+    -> forall t, has_ty M $0 e1 t
       -> compatible M env1
       -> compatible M env2.
   Proof.
@@ -1574,9 +1574,9 @@ Module StlcMutable.
       plug C e1 e1'
       -> forall e2 e2' t env1 env2, plug C e2 e2'
       -> step1 (env1, e1) (env2, e2)
-      -> hasty M $0 e1' t
+      -> has_ty M $0 e1' t
       -> compatible M env1
-      -> hasty M $0 e2' t.
+      -> has_ty M $0 e2' t.
   Proof.
     induct 1; t.
   Qed.
@@ -1586,7 +1586,7 @@ Module StlcMutable.
   Lemma preservation'_env' : forall M C e1 e1',
       plug C e1 e1'
       -> forall t e2 env1 env2, step1 (env1, e1) (env2, e2)
-      -> hasty M $0 e1' t
+      -> has_ty M $0 e1' t
       -> compatible M env1
       -> compatible M env2.
   Proof.
@@ -1596,7 +1596,7 @@ Module StlcMutable.
   Lemma preservation'_env : forall M C e1 e1' t e2 env1 env2,
       step1 (env1, e1) (env2, e2)
       -> plug C e1 e1'
-      -> hasty M $0 e1' t
+      -> has_ty M $0 e1' t
       -> compatible M env1
       -> compatible M env2.
   Proof.
@@ -1607,23 +1607,23 @@ Module StlcMutable.
   
   Lemma preservation : forall M env1 e1 env2 e2,
     step (env1, e1) (env2, e2)
-    -> forall t, hasty M $0 e1 t
+    -> forall t, has_ty M $0 e1 t
       -> compatible M env1
-      -> hasty M $0 e2 t /\ compatible M env2.
+      -> has_ty M $0 e2 t /\ compatible M env2.
   Proof.
     invert 1; t.
   Qed.
 
   Local Hint Resolve progress preservation : core.
 
-  Theorem safety : forall M env e t, hasty M $0 e t
+  Theorem safety : forall M env e t, has_ty M $0 e t
     -> compatible M env
     -> invariantFor (trsys_of env e)
                     (fun st => value (snd st)
                                \/ exists st', step st st').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun st => hasty M $0 (snd st) t /\ compatible M (fst st)); eauto.
+    apply invariant_weaken with (invariant1 := fun st => has_ty M $0 (snd st) t /\ compatible M (fst st)); eauto.
     apply invariant_induction; simplify.
     propositional; subst; auto.
     invert H1.
@@ -1818,64 +1818,64 @@ Module StlcConcur.
   | Prod (t1 t2 : type)
   | Sum (t1 t2 : type).
 
-  Inductive hasty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty M G (Var x) t
+    -> has_ty M G (Var x) t
   | HtConst : forall G n,
-    hasty M G (Const n) Nat
+    has_ty M G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty M G e1 Nat
-    -> hasty M G e2 Nat
-    -> hasty M G (Plus e1 e2) Nat
+    has_ty M G e1 Nat
+    -> has_ty M G e2 Nat
+    -> has_ty M G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty M (G $+ (x, t1)) e1 t2
-    -> hasty M G (Abs x e1) (Fun t1 t2)
+    has_ty M (G $+ (x, t1)) e1 t2
+    -> has_ty M G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty M G e1 (Fun t1 t2)
-    -> hasty M G e2 t1
-    -> hasty M G (App e1 e2) t2
+    has_ty M G e1 (Fun t1 t2)
+    -> has_ty M G e2 t1
+    -> has_ty M G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty M G e1 t1
-    -> hasty M G e2 t2
-    -> hasty M G (Pair e1 e2) (Prod t1 t2)
+    has_ty M G e1 t1
+    -> has_ty M G e2 t2
+    -> has_ty M G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Fst e1) t1
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Snd e1) t2
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Snd e1) t2
   | HtInl : forall G e1 t1 t2,
-      hasty M G e1 t1
-      -> hasty M G (Inl e1) (Sum t1 t2)
+      has_ty M G e1 t1
+      -> has_ty M G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty M G e1 t2
-      -> hasty M G (Inr e1) (Sum t1 t2)
+      has_ty M G e1 t2
+      -> has_ty M G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty M G e (Sum t1 t2)
-      -> hasty M (G $+ (x1, t1)) e1 t
-      -> hasty M (G $+ (x2, t2)) e2 t
-      -> hasty M G (Match e x1 e1 x2 e2) t
+      has_ty M G e (Sum t1 t2)
+      -> has_ty M (G $+ (x1, t1)) e1 t
+      -> has_ty M (G $+ (x2, t2)) e2 t
+      -> has_ty M G (Match e x1 e1 x2 e2) t
   | HtGetVar : forall G x t,
       M $? x = Some t
-      -> hasty M G (GetVar x) t
+      -> has_ty M G (GetVar x) t
   | HtSetVar : forall G x e t,
       M $? x = Some t
-      -> hasty M G e t
-      -> hasty M G (SetVar x e) t
+      -> has_ty M G e t
+      -> has_ty M G (SetVar x e) t
 
   (* New cases: *)
   | HtPar : forall G e1 t1 e2 t2,
-      hasty M G e1 t1
-      -> hasty M G e2 t2
-      -> hasty M G (Par e1 e2) (Prod t1 t2).
+      has_ty M G e1 t1
+      -> has_ty M G e2 t2
+      -> has_ty M G (Par e1 e2) (Prod t1 t2).
                
-  Local Hint Constructors value plug step0 step1 step hasty : core.
+  Local Hint Constructors value plug step0 step1 step has_ty : core.
 
   Definition compatible (M : fmap var type) (env : valuation) :=
     forall x t, M $? x = Some t
                 -> exists v, env $? x = Some v
-                             /\ hasty M $0 v t.
+                             /\ has_ty M $0 v t.
   
   Ltac t0 := match goal with
              | [ H : ex _ |- _ ] => invert H
@@ -1885,10 +1885,10 @@ Module StlcConcur.
 
              | [ H : step _ _ |- _ ] => invert H
              | [ H : step0 _ _ |- _ ] => invert1 H
-             | [ H : hasty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
-             | [ H : hasty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
+             | [ H : has_ty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; []
+             | [ H : has_ty _ _ ?e _, H' : value ?e |- _ ] => invert H'; invert H; [|]
 
-             | [ H : hasty _ _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ _ _ _ |- _ ] => invert1 H
              | [ H : plug _ _ _ |- _ ] => invert1 H
 
              | [ H1 : compatible ?M ?env, H2 : ?M $? ?x = Some _ |- _ ] =>
@@ -1901,7 +1901,7 @@ Module StlcConcur.
   Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 7.
   
   Lemma progress : forall M e t,
-    hasty M $0 e t
+    has_ty M $0 e t
     -> forall env, compatible M env
     -> value e
     \/ exists st', step (env, e) st'.
@@ -1920,29 +1920,29 @@ Module StlcConcur.
 
   Local Hint Resolve weakening_override : core.
 
-  Lemma weakening : forall M G e t, hasty M G e t
+  Lemma weakening : forall M G e t, has_ty M G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty M G' e t.
+      -> has_ty M G' e t.
   Proof.
     induct 1; t.
   Qed.
 
   Local Hint Resolve weakening : core.
 
-  Lemma hasty_change : forall M G e t,
-    hasty M G e t
+  Lemma has_ty_change : forall M G e t,
+    has_ty M G e t
     -> forall G', G' = G
-      -> hasty M G' e t.
+      -> has_ty M G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution : forall M G x t' e t e',
-    hasty M (G $+ (x, t')) e t
-    -> hasty M $0 e' t'
-    -> hasty M G (subst e' x e) t.
+    has_ty M (G $+ (x, t')) e t
+    -> has_ty M $0 e' t'
+    -> has_ty M G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -1952,7 +1952,7 @@ Module StlcConcur.
   Lemma compatible_bind : forall M env x v t,
       compatible M env
       -> M $? x = Some t
-      -> hasty M $0 v t
+      -> has_ty M $0 v t
       -> compatible M (env $+ (x, v)).
   Proof.
     unfold compatible; first_order.
@@ -1965,11 +1965,11 @@ Module StlcConcur.
 
   Local Hint Resolve compatible_bind : core.
 
-  Lemma compatible_hasty : forall M env x v t,
+  Lemma compatible_has_ty : forall M env x v t,
       compatible M env
       -> env $? x = Some v
       -> M $? x = Some t
-      -> hasty M $0 v t.
+      -> has_ty M $0 v t.
   Proof.
     t.
     specialize (H _ _ H1); first_order.
@@ -1978,12 +1978,12 @@ Module StlcConcur.
     assumption.
   Qed.
 
-  Local Hint Immediate compatible_hasty : core.
+  Local Hint Immediate compatible_has_ty : core.
   
   Lemma preservation0 : forall M e1 e2,
     step0 e1 e2
-    -> forall t, hasty M $0 e1 t
-      -> hasty M $0 e2 t.
+    -> forall t, has_ty M $0 e1 t
+      -> has_ty M $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
@@ -1992,16 +1992,16 @@ Module StlcConcur.
   
   Lemma preservation1_exp : forall M env1 e1 env2 e2,
     step1 (env1, e1) (env2, e2)
-    -> forall t, hasty M $0 e1 t
+    -> forall t, has_ty M $0 e1 t
       -> compatible M env1
-      -> hasty M $0 e2 t.
+      -> has_ty M $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
 
   Lemma preservation1_env : forall M env1 e1 env2 e2,
     step1 (env1, e1) (env2, e2)
-    -> forall t, hasty M $0 e1 t
+    -> forall t, has_ty M $0 e1 t
       -> compatible M env1
       -> compatible M env2.
   Proof.
@@ -2014,9 +2014,9 @@ Module StlcConcur.
       plug C e1 e1'
       -> forall e2 e2' t env1 env2, plug C e2 e2'
       -> step1 (env1, e1) (env2, e2)
-      -> hasty M $0 e1' t
+      -> has_ty M $0 e1' t
       -> compatible M env1
-      -> hasty M $0 e2' t.
+      -> has_ty M $0 e2' t.
   Proof.
     induct 1; t.
   Qed.
@@ -2026,7 +2026,7 @@ Module StlcConcur.
   Lemma preservation'_env' : forall M C e1 e1',
       plug C e1 e1'
       -> forall t e2 env1 env2, step1 (env1, e1) (env2, e2)
-      -> hasty M $0 e1' t
+      -> has_ty M $0 e1' t
       -> compatible M env1
       -> compatible M env2.
   Proof.
@@ -2036,7 +2036,7 @@ Module StlcConcur.
   Lemma preservation'_env : forall M C e1 e1' t e2 env1 env2,
       step1 (env1, e1) (env2, e2)
       -> plug C e1 e1'
-      -> hasty M $0 e1' t
+      -> has_ty M $0 e1' t
       -> compatible M env1
       -> compatible M env2.
   Proof.
@@ -2047,23 +2047,23 @@ Module StlcConcur.
   
   Lemma preservation : forall M env1 e1 env2 e2,
     step (env1, e1) (env2, e2)
-    -> forall t, hasty M $0 e1 t
+    -> forall t, has_ty M $0 e1 t
       -> compatible M env1
-      -> hasty M $0 e2 t /\ compatible M env2.
+      -> has_ty M $0 e2 t /\ compatible M env2.
   Proof.
     invert 1; t.
   Qed.
 
   Local Hint Resolve progress preservation : core.
 
-  Theorem safety : forall M env e t, hasty M $0 e t
+  Theorem safety : forall M env e t, has_ty M $0 e t
     -> compatible M env
     -> invariantFor (trsys_of env e)
                     (fun st => value (snd st)
                                \/ exists st', step st st').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun st => hasty M $0 (snd st) t /\ compatible M (fst st)); eauto.
+    apply invariant_weaken with (invariant1 := fun st => has_ty M $0 (snd st) t /\ compatible M (fst st)); eauto.
     apply invariant_induction; simplify.
     propositional; subst; auto.
     invert H1.
diff --git a/EvaluationContexts_template.v b/EvaluationContexts_template.v
index 7430e9d..6918536 100644
--- a/EvaluationContexts_template.v
+++ b/EvaluationContexts_template.v
@@ -80,25 +80,25 @@ Module Stlc.
   | Nat                  (* Numbers *)
   | Fun (dom ran : type) (* Functions *).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2.
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2.
 
-  Local Hint Constructors value plug step0 step hasty : core.
+  Local Hint Constructors value plug step0 step has_ty : core.
 
   (** * Now we adapt the automated proof of type soundness. *)
 
@@ -110,15 +110,15 @@ Module Stlc.
 
              | [ H : step _ _ |- _ ] => invert H
              | [ H : step0 _ _ |- _ ] => invert1 H
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
-             | [ H : hasty _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
+             | [ H : has_ty _ _ _ |- _ ] => invert1 H
              | [ H : plug _ _ _ |- _ ] => invert1 H
              end; subst.
 
   Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
 
   Lemma progress : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> value e
     \/ (exists e' : exp, step e e').
   Proof.
@@ -137,29 +137,29 @@ Module Stlc.
   Local Hint Resolve weakening_override : core.
 
   Lemma weakening : forall G e t,
-    hasty G e t
+    has_ty G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     induct 1; t.
   Qed.
 
   Local Hint Resolve weakening : core.
 
-  Lemma hasty_change : forall G e t,
-    hasty G e t
+  Lemma has_ty_change : forall G e t,
+    has_ty G e t
     -> forall G', G' = G
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution : forall G x t' e t e',
-    hasty (G $+ (x, t')) e t
-    -> hasty $0 e' t'
-    -> hasty G (subst e' x e) t.
+    has_ty (G $+ (x, t')) e t
+    -> has_ty $0 e' t'
+    -> has_ty G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -168,8 +168,8 @@ Module Stlc.
 
   Lemma preservation0 : forall e1 e2,
     step0 e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
@@ -180,8 +180,8 @@ Module Stlc.
       plug C e1 e1'
       -> forall e2 e2' t, plug C e2 e2'
       -> step0 e1 e2
-      -> hasty $0 e1' t
-      -> hasty $0 e2' t.
+      -> has_ty $0 e1' t
+      -> has_ty $0 e2' t.
   Proof.
     induct 1; t.
   Qed.
@@ -190,21 +190,21 @@ Module Stlc.
   
   Lemma preservation : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     invert 1; t.
   Qed.
 
   Local Hint Resolve progress preservation : core.
 
-  Theorem safety : forall e t, hasty $0 e t
+  Theorem safety : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e)
                     (fun e' => value e'
                                \/ exists e'', step e' e'').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
 
@@ -390,33 +390,33 @@ Module StlcPairs.
   | Fun (dom ran : type)
   | Prod (t1 t2 : type) (* "Prod" for "product," as in Cartesian product *).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty G e1 t1
-    -> hasty G e2 t2
-    -> hasty G (Pair e1 e2) (Prod t1 t2)
+    has_ty G e1 t1
+    -> has_ty G e2 t2
+    -> has_ty G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Fst e1) t1
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Snd e1) t2.
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Snd e1) t2.
 
   (* Let's copy and paste the type-soundness proof from above and adapt it. *)
 End StlcPairs.
@@ -567,46 +567,46 @@ Module StlcSums.
   (* New case: *)
   | Sum (t1 t2 : type).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty G e1 t1
-    -> hasty G e2 t2
-    -> hasty G (Pair e1 e2) (Prod t1 t2)
+    has_ty G e1 t1
+    -> has_ty G e2 t2
+    -> has_ty G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Fst e1) t1
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Snd e1) t2
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Snd e1) t2
 
   (* New cases: *)
   | HtInl : forall G e1 t1 t2,
-      hasty G e1 t1
-      -> hasty G (Inl e1) (Sum t1 t2)
+      has_ty G e1 t1
+      -> has_ty G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty G e1 t2
-      -> hasty G (Inr e1) (Sum t1 t2)
+      has_ty G e1 t2
+      -> has_ty G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty G e (Sum t1 t2)
-      -> hasty (G $+ (x1, t1)) e1 t
-      -> hasty (G $+ (x2, t2)) e2 t
-      -> hasty G (Match e x1 e1 x2 e2) t.
+      has_ty G e (Sum t1 t2)
+      -> has_ty (G $+ (x1, t1)) e1 t
+      -> has_ty (G $+ (x2, t2)) e2 t
+      -> has_ty G (Match e x1 e1 x2 e2) t.
 
   (* Type-soundness proof here *)
 End StlcSums.
@@ -777,53 +777,53 @@ Module StlcExceptions.
   | Prod (t1 t2 : type)
   | Sum (t1 t2 : type).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty G e1 t1
-    -> hasty G e2 t2
-    -> hasty G (Pair e1 e2) (Prod t1 t2)
+    has_ty G e1 t1
+    -> has_ty G e2 t2
+    -> has_ty G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Fst e1) t1
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty G e1 (Prod t1 t2)
-    -> hasty G (Snd e1) t2
+    has_ty G e1 (Prod t1 t2)
+    -> has_ty G (Snd e1) t2
   | HtInl : forall G e1 t1 t2,
-      hasty G e1 t1
-      -> hasty G (Inl e1) (Sum t1 t2)
+      has_ty G e1 t1
+      -> has_ty G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty G e1 t2
-      -> hasty G (Inr e1) (Sum t1 t2)
+      has_ty G e1 t2
+      -> has_ty G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty G e (Sum t1 t2)
-      -> hasty (G $+ (x1, t1)) e1 t
-      -> hasty (G $+ (x2, t2)) e2 t
-      -> hasty G (Match e x1 e1 x2 e2) t
+      has_ty G e (Sum t1 t2)
+      -> has_ty (G $+ (x1, t1)) e1 t
+      -> has_ty (G $+ (x2, t2)) e2 t
+      -> has_ty G (Match e x1 e1 x2 e2) t
 
   (* New cases: *)
   | HtThrow : forall G e1 t,
-      hasty G e1 Nat
-      -> hasty G (Throw e1) t
+      has_ty G e1 Nat
+      -> has_ty G (Throw e1) t
   | HtCatch : forall G e x1 e1 t,
-      hasty G e t
-      -> hasty (G $+ (x1, Nat)) e1 t
-      -> hasty G (Catch e x1 e1) t.
+      has_ty G e t
+      -> has_ty (G $+ (x1, Nat)) e1 t
+      -> has_ty G (Catch e x1 e1) t.
 End StlcExceptions.
 
 (** * Mutable Variables *)
@@ -991,53 +991,53 @@ Module StlcMutable.
 
   (* Now there will be two typing contexts, one for mutable variables and one
    * for immutable. *)
-  Inductive hasty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty M G (Var x) t
+    -> has_ty M G (Var x) t
   | HtConst : forall G n,
-    hasty M G (Const n) Nat
+    has_ty M G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty M G e1 Nat
-    -> hasty M G e2 Nat
-    -> hasty M G (Plus e1 e2) Nat
+    has_ty M G e1 Nat
+    -> has_ty M G e2 Nat
+    -> has_ty M G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty M (G $+ (x, t1)) e1 t2
-    -> hasty M G (Abs x e1) (Fun t1 t2)
+    has_ty M (G $+ (x, t1)) e1 t2
+    -> has_ty M G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty M G e1 (Fun t1 t2)
-    -> hasty M G e2 t1
-    -> hasty M G (App e1 e2) t2
+    has_ty M G e1 (Fun t1 t2)
+    -> has_ty M G e2 t1
+    -> has_ty M G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty M G e1 t1
-    -> hasty M G e2 t2
-    -> hasty M G (Pair e1 e2) (Prod t1 t2)
+    has_ty M G e1 t1
+    -> has_ty M G e2 t2
+    -> has_ty M G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Fst e1) t1
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Snd e1) t2
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Snd e1) t2
   | HtInl : forall G e1 t1 t2,
-      hasty M G e1 t1
-      -> hasty M G (Inl e1) (Sum t1 t2)
+      has_ty M G e1 t1
+      -> has_ty M G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty M G e1 t2
-      -> hasty M G (Inr e1) (Sum t1 t2)
+      has_ty M G e1 t2
+      -> has_ty M G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty M G e (Sum t1 t2)
-      -> hasty M (G $+ (x1, t1)) e1 t
-      -> hasty M (G $+ (x2, t2)) e2 t
-      -> hasty M G (Match e x1 e1 x2 e2) t
+      has_ty M G e (Sum t1 t2)
+      -> has_ty M (G $+ (x1, t1)) e1 t
+      -> has_ty M (G $+ (x2, t2)) e2 t
+      -> has_ty M G (Match e x1 e1 x2 e2) t
 
   (* New cases: *)
   | HtGetVar : forall G x t,
       M $? x = Some t
-      -> hasty M G (GetVar x) t
+      -> has_ty M G (GetVar x) t
   | HtSetVar : forall G x e t,
       M $? x = Some t
-      -> hasty M G e t
-      -> hasty M G (SetVar x e) t.
+      -> has_ty M G e t
+      -> has_ty M G (SetVar x e) t.
 End StlcMutable.
 
 (** * Concurrency *)
@@ -1218,57 +1218,57 @@ Module StlcConcur.
   | Prod (t1 t2 : type)
   | Sum (t1 t2 : type).
 
-  Inductive hasty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty (M : fmap var type) : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty M G (Var x) t
+    -> has_ty M G (Var x) t
   | HtConst : forall G n,
-    hasty M G (Const n) Nat
+    has_ty M G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty M G e1 Nat
-    -> hasty M G e2 Nat
-    -> hasty M G (Plus e1 e2) Nat
+    has_ty M G e1 Nat
+    -> has_ty M G e2 Nat
+    -> has_ty M G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty M (G $+ (x, t1)) e1 t2
-    -> hasty M G (Abs x e1) (Fun t1 t2)
+    has_ty M (G $+ (x, t1)) e1 t2
+    -> has_ty M G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty M G e1 (Fun t1 t2)
-    -> hasty M G e2 t1
-    -> hasty M G (App e1 e2) t2
+    has_ty M G e1 (Fun t1 t2)
+    -> has_ty M G e2 t1
+    -> has_ty M G (App e1 e2) t2
   | HtPair : forall G e1 e2 t1 t2,
-    hasty M G e1 t1
-    -> hasty M G e2 t2
-    -> hasty M G (Pair e1 e2) (Prod t1 t2)
+    has_ty M G e1 t1
+    -> has_ty M G e2 t2
+    -> has_ty M G (Pair e1 e2) (Prod t1 t2)
   | HtFst : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Fst e1) t1
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Fst e1) t1
   | HtSnd : forall G e1 t1 t2,
-    hasty M G e1 (Prod t1 t2)
-    -> hasty M G (Snd e1) t2
+    has_ty M G e1 (Prod t1 t2)
+    -> has_ty M G (Snd e1) t2
   | HtInl : forall G e1 t1 t2,
-      hasty M G e1 t1
-      -> hasty M G (Inl e1) (Sum t1 t2)
+      has_ty M G e1 t1
+      -> has_ty M G (Inl e1) (Sum t1 t2)
   | HtInr : forall G e1 t1 t2,
-      hasty M G e1 t2
-      -> hasty M G (Inr e1) (Sum t1 t2)
+      has_ty M G e1 t2
+      -> has_ty M G (Inr e1) (Sum t1 t2)
   | HtMatch : forall G e t1 t2 x1 e1 x2 e2 t,
-      hasty M G e (Sum t1 t2)
-      -> hasty M (G $+ (x1, t1)) e1 t
-      -> hasty M (G $+ (x2, t2)) e2 t
-      -> hasty M G (Match e x1 e1 x2 e2) t
+      has_ty M G e (Sum t1 t2)
+      -> has_ty M (G $+ (x1, t1)) e1 t
+      -> has_ty M (G $+ (x2, t2)) e2 t
+      -> has_ty M G (Match e x1 e1 x2 e2) t
   | HtGetVar : forall G x t,
       M $? x = Some t
-      -> hasty M G (GetVar x) t
+      -> has_ty M G (GetVar x) t
   | HtSetVar : forall G x e t,
       M $? x = Some t
-      -> hasty M G e t
-      -> hasty M G (SetVar x e) t
+      -> has_ty M G e t
+      -> has_ty M G (SetVar x e) t
 
   (* New cases: *)
   | HtPar : forall G e1 t1 e2 t2,
-      hasty M G e1 t1
-      -> hasty M G e2 t2
-      -> hasty M G (Par e1 e2) (Prod t1 t2).
+      has_ty M G e1 t1
+      -> has_ty M G e2 t2
+      -> has_ty M G (Par e1 e2) (Prod t1 t2).
 
   (* Type-soundness proof *)
 End StlcConcur.
diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v
index 66e9c20..87c380c 100644
--- a/LambdaCalculusAndTypeSoundness.v
+++ b/LambdaCalculusAndTypeSoundness.v
@@ -477,25 +477,25 @@ Module Stlc.
    * (not to be confused with evaluation contexts) to map free variables to
    * their types.  Free variables are those that don't refer to enclosing [Abs]
    * binders. *)
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2.
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2.
 
-  Local Hint Constructors value step hasty : core.
+  Local Hint Constructors value step has_ty : core.
 
   (* Some notation to make it more pleasant to write programs *)
   Infix "-->" := Fun (at level 60, right associativity).
@@ -507,22 +507,22 @@ Module Stlc.
 
   (* Some examples of typed programs *)
 
-  Example one_plus_one : hasty $0 (1 ^+^ 1) Nat.
+  Example one_plus_one : has_ty $0 (1 ^+^ 1) Nat.
   Proof.
     repeat (econstructor; simplify).
   Qed.
 
-  Example add : hasty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat).
+  Example add : has_ty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat).
   Proof.
     repeat (econstructor; simplify).
   Qed.
 
-  Example eleven : hasty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat.
+  Example eleven : has_ty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat.
   Proof.
     repeat (econstructor; simplify).
   Qed.
 
-  Example seven_the_long_way : hasty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat.
+  Example seven_the_long_way : has_ty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat.
   Proof.
     repeat (econstructor; simplify).
   Qed.
@@ -542,7 +542,7 @@ Module Stlc.
   (* Now we're ready for the first of the two key properties to establish that
    * invariant: well-typed programs are never stuck. *)
   Lemma progress : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> unstuck e.
   Proof.
     unfold unstuck; induct 1; simplify; try equality.
@@ -556,10 +556,10 @@ Module Stlc.
     (* Some automation is needed here to maintain compatibility with
      * name generation in different Coq versions. *)
     match goal with
-    | [ H1 : value e1, H2 : hasty $0 e1 _ |- _ ] => invert H1; invert H2
+    | [ H1 : value e1, H2 : has_ty $0 e1 _ |- _ ] => invert H1; invert H2
     end.
     match goal with
-    | [ H1 : value e2, H2 : hasty $0 e2 _ |- _ ] => invert H1; invert H2
+    | [ H1 : value e2, H2 : has_ty $0 e2 _ |- _ ] => invert H1; invert H2
     end.
     exists (Const (n + n0)).
     constructor.
@@ -596,7 +596,7 @@ Module Stlc.
 
     right.
     match goal with
-    | [ H1 : value e1, H2 : hasty $0 e1 _ |- _ ] => invert H1; invert H2
+    | [ H1 : value e1, H2 : has_ty $0 e1 _ |- _ ] => invert H1; invert H2
     end.
     exists (subst e2 x e0).
     constructor.
@@ -643,9 +643,9 @@ Module Stlc.
   (* This lemma lets us transplant a typing derivation into a new context that
    * includes the old one. *)
   Lemma weakening : forall G e t,
-    hasty G e t
+    has_ty G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     induct 1; simplify.
 
@@ -656,28 +656,28 @@ Module Stlc.
     constructor.
 
     constructor.
-    apply IHhasty1.
+    apply IHhas_ty1.
     assumption.
-    apply IHhasty2.
+    apply IHhas_ty2.
     assumption.
 
     constructor.
-    apply IHhasty.
+    apply IHhas_ty.
     apply weakening_override.
     assumption.
 
     econstructor.
-    apply IHhasty1.
+    apply IHhas_ty1.
     assumption.
-    apply IHhasty2.
+    apply IHhas_ty2.
     assumption.
   Qed.
 
   (* Replacing a variable with a properly typed term preserves typing. *)
   Lemma substitution : forall G x t' e t e',
-    hasty (G $+ (x, t')) e t
-    -> hasty $0 e' t'
-    -> hasty G (subst e' x e) t.
+    has_ty (G $+ (x, t')) e t
+    -> has_ty $0 e' t'
+    -> has_ty G (subst e' x e) t.
   Proof.
     induct 1; simplify.
 
@@ -697,8 +697,8 @@ Module Stlc.
     constructor.
 
     constructor.
-    eapply IHhasty1; equality.
-    eapply IHhasty2; equality.
+    eapply IHhas_ty1; equality.
+    eapply IHhas_ty2; equality.
 
     cases (x0 ==v x).
 
@@ -715,20 +715,20 @@ Module Stlc.
     assumption.
 
     constructor.
-    eapply IHhasty.
+    eapply IHhas_ty.
     maps_equal.
     assumption.
 
     econstructor.
-    eapply IHhasty1; equality.
-    eapply IHhasty2; equality.
+    eapply IHhas_ty1; equality.
+    eapply IHhas_ty2; equality.
   Qed.
 
   (* OK, now we're almost done.  Full steps really do preserve typing! *)
   Lemma preservation : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     induct 1; simplify.
 
@@ -770,7 +770,7 @@ Module Stlc.
    * presented from scratch as a proof technique, it turns out that the two key
    * properties, progress and preservation, are just instances of the same methods
    * we've been applying all along with invariants of transition systems! *)
-  Theorem safety : forall e t, hasty $0 e t
+  Theorem safety : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e) unstuck.
   Proof.
     simplify.
@@ -778,7 +778,7 @@ Module Stlc.
     (* Step 1: strengthen the invariant.  In particular, the typing relation is
      * exactly the right stronger invariant!  Our progress theorem proves the
      * required invariant inclusion. *)
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t).
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t).
 
     (* Step 2: apply invariant induction, whose induction step turns out to match
      * our preservation theorem exactly! *)
@@ -805,14 +805,14 @@ Module Stlc.
              | [ H : Some _ = Some _ |- _ ] => invert H
 
              | [ H : step _ _ |- _ ] => invert1 H
-             | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
-             | [ H : hasty _ _ _ |- _ ] => invert1 H
+             | [ H : has_ty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
+             | [ H : has_ty _ _ _ |- _ ] => invert1 H
              end; subst.
 
   Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
 
   Lemma progress_snazzy : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> value e
     \/ (exists e' : exp, step e e').
   Proof.
@@ -822,9 +822,9 @@ Module Stlc.
   Local Hint Resolve weakening_override : core.
 
   Lemma weakening_snazzy : forall G e t,
-    hasty G e t
+    has_ty G e t
     -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     induct 1; t.
   Qed.
@@ -833,20 +833,20 @@ Module Stlc.
 
   (* Replacing a typing context with an equal one has no effect (useful to guide
    * proof search as a hint). *)
-  Lemma hasty_change : forall G e t,
-    hasty G e t
+  Lemma has_ty_change : forall G e t,
+    has_ty G e t
     -> forall G', G' = G
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
     t.
   Qed.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma substitution_snazzy : forall G x t' e t e',
-    hasty (G $+ (x, t')) e t
-    -> hasty $0 e' t'
-    -> hasty G (subst e' x e) t.
+    has_ty (G $+ (x, t')) e t
+    -> has_ty $0 e' t'
+    -> has_ty G (subst e' x e) t.
   Proof.
     induct 1; t.
   Qed.
@@ -855,21 +855,21 @@ Module Stlc.
 
   Lemma preservation_snazzy : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
     induct 1; t.
   Qed.
 
   Local Hint Resolve progress_snazzy preservation_snazzy : core.
 
-  Theorem safety_snazzy : forall e t, hasty $0 e t
+  Theorem safety_snazzy : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e)
                     (fun e' => value e'
                                \/ exists e'', step e' e'').
   Proof.
     simplify.
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t); eauto.
     apply invariant_induction; simplify; eauto; equality.
   Qed.
 End Stlc.
diff --git a/LambdaCalculusAndTypeSoundness_template.v b/LambdaCalculusAndTypeSoundness_template.v
index 8950521..337df25 100644
--- a/LambdaCalculusAndTypeSoundness_template.v
+++ b/LambdaCalculusAndTypeSoundness_template.v
@@ -419,25 +419,25 @@ Module Stlc.
   | Nat                  (* Numbers *)
   | Fun (dom ran : type) (* Functions *).
 
-  Inductive hasty : fmap var type -> exp -> type -> Prop :=
+  Inductive has_ty : fmap var type -> exp -> type -> Prop :=
   | HtVar : forall G x t,
     G $? x = Some t
-    -> hasty G (Var x) t
+    -> has_ty G (Var x) t
   | HtConst : forall G n,
-    hasty G (Const n) Nat
+    has_ty G (Const n) Nat
   | HtPlus : forall G e1 e2,
-    hasty G e1 Nat
-    -> hasty G e2 Nat
-    -> hasty G (Plus e1 e2) Nat
+    has_ty G e1 Nat
+    -> has_ty G e2 Nat
+    -> has_ty G (Plus e1 e2) Nat
   | HtAbs : forall G x e1 t1 t2,
-    hasty (G $+ (x, t1)) e1 t2
-    -> hasty G (Abs x e1) (Fun t1 t2)
+    has_ty (G $+ (x, t1)) e1 t2
+    -> has_ty G (Abs x e1) (Fun t1 t2)
   | HtApp : forall G e1 e2 t1 t2,
-    hasty G e1 (Fun t1 t2)
-    -> hasty G e2 t1
-    -> hasty G (App e1 e2) t2.
+    has_ty G e1 (Fun t1 t2)
+    -> has_ty G e2 t1
+    -> has_ty G (App e1 e2) t2.
 
-  Local Hint Constructors value step hasty : core.
+  Local Hint Constructors value step has_ty : core.
 
   (* Some notation to make it more pleasant to write programs *)
   Infix "-->" := Fun (at level 60, right associativity).
@@ -449,22 +449,22 @@ Module Stlc.
 
   (* Some examples of typed programs *)
 
-  Example one_plus_one : hasty $0 (1 ^+^ 1) Nat.
+  Example one_plus_one : has_ty $0 (1 ^+^ 1) Nat.
   Proof.
     repeat (econstructor; simplify).
   Qed.
 
-  Example add : hasty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat).
+  Example add : has_ty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat).
   Proof.
     repeat (econstructor; simplify).
   Qed.
 
-  Example eleven : hasty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat.
+  Example eleven : has_ty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat.
   Proof.
     repeat (econstructor; simplify).
   Qed.
 
-  Example seven_the_long_way : hasty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat.
+  Example seven_the_long_way : has_ty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat.
   Proof.
     repeat (econstructor; simplify).
   Qed.
@@ -476,7 +476,7 @@ Module Stlc.
     \/ (exists e' : exp, step e e').
 
   Lemma progress : forall e t,
-    hasty $0 e t
+    has_ty $0 e t
     -> value e
     \/ (exists e' : exp, step e e').
   Proof.
@@ -484,23 +484,23 @@ Module Stlc.
 
   (* Replacing a typing context with an equal one has no effect (useful to guide
    * proof search as a hint). *)
-  Lemma hasty_change : forall G e t,
-    hasty G e t
+  Lemma has_ty_change : forall G e t,
+    has_ty G e t
     -> forall G', G' = G
-      -> hasty G' e t.
+      -> has_ty G' e t.
   Proof.
   Admitted.
 
-  Local Hint Resolve hasty_change : core.
+  Local Hint Resolve has_ty_change : core.
 
   Lemma preservation : forall e1 e2,
     step e1 e2
-    -> forall t, hasty $0 e1 t
-      -> hasty $0 e2 t.
+    -> forall t, has_ty $0 e1 t
+      -> has_ty $0 e2 t.
   Proof.
   Admitted.
 
-  Theorem safety : forall e t, hasty $0 e t
+  Theorem safety : forall e t, has_ty $0 e t
     -> invariantFor (trsys_of e) unstuck.
   Proof.
     simplify.
@@ -508,7 +508,7 @@ Module Stlc.
     (* Step 1: strengthen the invariant.  In particular, the typing relation is
      * exactly the right stronger invariant!  Our progress theorem proves the
      * required invariant inclusion. *)
-    apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t).
+    apply invariant_weaken with (invariant1 := fun e' => has_ty $0 e' t).
 
     (* Step 2: apply invariant induction, whose induction step turns out to match
      * our preservation theorem exactly! *)