Update

src/subsequences2.v

@@ -384,30 +384,24 @@ Qed.
  Theorem Subsequence_in {X: Type} :
    forall (u: list X) a, In a u <-> Subsequence u [a].
  Proof.
-   intros u a. rewrite Subsequence_flat_map. split.
+   intros u a. split. induction u; intro H.
-   induction u; intro H. apply in_nil in H. contradiction.
+   apply in_nil in H. contradiction.
-   destruct H. rewrite H. exists nil. exists [u]. split. reflexivity.
+   destruct H. rewrite H. exists nil. exists u.
-   simpl. rewrite app_nil_r. reflexivity.
+   split. reflexivity. apply Subsequence_nil_r.
-   rewrite <- Subsequence_flat_map. apply Subsequence_cons_l.
+   apply Subsequence_cons_l. apply IHu. assumption.
-   apply Subsequence_flat_map. apply IHu. assumption.
+   intro H. destruct H. destruct H. destruct H. rewrite H.
-   intro H. destruct H. destruct H. destruct H. rewrite H0. apply in_or_app.
+   apply in_or_app. right. apply in_eq.
-   right. destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
-   left. reflexivity.
 Qed.
 
 
-
+Theorem Subsequence_rev {X: Type} :
-
+  forall (u v: list X), Subsequence u v <-> Subsequence (rev u) (rev v).
-
-
-Theorem subsequence_rev {X: Type} :
-  forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
 Proof.
   assert (MAIN: forall (u v: list X),
-      subsequence u v -> subsequence (rev u) (rev v)).
+      Subsequence u v -> Subsequence (rev u) (rev v)).
   intros u v. intro H.
-  apply subsequence_eq_def_3. apply subsequence_eq_def_2.
+  apply Subsequence_bools. apply Subsequence_bools in H.
-  apply subsequence_eq_def_1 in H. destruct H. destruct H.
+  destruct H. destruct H.
   exists (rev x). split. rewrite rev_length. rewrite rev_length.
   assumption. rewrite H0.
 
@@ -439,6 +433,9 @@ Proof.
 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).