diff --git a/src/subsequences.v b/src/subsequences.v
index 8744dd4..4af27af 100644
--- a/src/subsequences.v
+++ b/src/subsequences.v
@@ -586,9 +586,8 @@ Qed.
 Theorem subsequence_map {X Y: Type} :
   forall (u v: list X) (f: X -> Y),
     subsequence u v -> subsequence (map f u) (map f v).
-  intros u v. generalize u. induction v; intros u0 f.
-  intro. apply subsequence_nil_r. intro H.
-  apply subsequence_eq_def_3.
+  intros u v. generalize u. induction v; intros u0 f; intro H.
+  apply subsequence_nil_r. apply subsequence_eq_def_3.
   apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
   destruct H. destruct H. destruct H.
   exists (map f x). exists (map f x0). split.
@@ -755,8 +754,8 @@ Qed.
 Theorem subsequence_add {X: Type} :
   forall (u v w: list X) x, subsequence u v -> Add x u w -> subsequence w v.
 Proof.
-  intros u v w. generalize u v. induction w; intros u0 v0 x; intro H.
-  intro I. inversion I. intro I.  inversion I.
+  intros u v w. generalize u v.
+  induction w; intros u0 v0 x; intros H I; inversion I.
   rewrite <- H2. apply subsequence_cons_l. rewrite <- H3. assumption.
 
   assert (J := H). apply subsequence_eq_def_1 in H. rewrite <- H1 in H.