Fix broken scripts in 8.4pl5

Author: alxest

StlcProp.v

@@ -801,8 +801,8 @@ Theorem types_unique' : forall Gamma t T,
 Proof with eauto.
   intros.
   generalize dependent T'.
-  induction H; intros...; inv H0.
-  inv H0. rewrite H in H3. inversion H3...
+  induction H; intros... inv H0.
+  rewrite H in H3. inversion H3...
   inv H0. apply IHhas_type in H6. subst...
   inv H1. apply IHhas_type1 in H5. inversion H5...
   inv H0...
@@ -1518,9 +1518,9 @@ Proof with auto.
   unfold deterministic.
   intros.
   generalize dependent y2.
-  induction H; intros...; inv H0...
+  induction H; intros... inv H0...
 
-  inv H0. auto. inv H3. inv H... inv H5... inv H5. inv H5.
+   auto. inv H3. inv H... inv H5... inv H5. inv H5.
 
   inv H1... inv H... inv H5...
   inv H0... inv H0. inv H0. apply IHstep in H6. subst...
@@ -2937,7 +2937,7 @@ Proof with eauto.
   unfold deterministic.
   intros.
   generalize dependent y2.
-  step_cases (induction H) Case; intros...; inv H0...
+  step_cases (induction H) Case; intros... 
 (*  induction H; intros...; inv H0... *)
   Case "ST_AppAbs".
   inv H0... inv H4... inv H3.