Clean up exercises01 a bit, add them to _CoqProject

_CoqProject

@@ -19,5 +19,5 @@ theories/type_systems/stlc/notation.v
 # By removing the # below, you can add the exercise sheets to make
 theories/type_systems/warmup/warmup.v
 #theories/type_systems/warmup/warmup_sol.v
-#theories/type_systems/stlc/exercises01.v
+theories/type_systems/stlc/exercises01.v
 #theories/type_systems/stlc/exercises01_sol.v

theories/type_systems/stlc/exercises01.v

@@ -68,13 +68,15 @@ Proof.
     | e_l e_l' e_r H_val H_l_step IH
     | e_l e_r e_r' H_r_step IH
   ]; subst.
-  all: intros e' H_step'; inversion H_step'; subst; try val_no_step.
-  - reflexivity.
-  - by rewrite (IH e1').
-  - by rewrite (IH e2').
-  - reflexivity.
-  - by rewrite (IH e1').
-  - by rewrite (IH e2').
+  all: intros e' H_step'; inversion H_step' as [
+    |
+    _tmp e_ind |
+    _tmp1 _tmp2 e_ind |
+    |
+    _tmp e_ind |
+    _tmp1 _tmp2 e_ind
+  ]; subst; intuition try val_no_step.
+  all: by rewrite (IH e_ind).
 Qed.
 
 (** Exercise 3 (LN Exercise 2): Call-by-name Semantics *)