Update

src/subsequences.v

@@ -507,6 +507,29 @@ Proof.
   contradiction H5. assumption.
 Qed.
 
+
+Theorem subsequence_length_eq {X: Type} :
+  forall (u v: list X),
+  subsequence u v -> length u = length v -> u = v.
+Proof.
+  intros u v. intros H I. apply subsequence_eq_def_1 in H.
+  destruct H. destruct H. rewrite H0 in I.
+  rewrite map_length in I.
+  replace (length u) with (length (combine x u)) in I.
+  symmetry in I. apply filter_length_forallb in I.
+  apply forallb_filter_id in I. rewrite I in H0.
+
+  assert (J: forall (a: list bool) (b: list X),
+    length a = length b -> b = map snd (combine a b)).
+  intro a. induction a; intro b; intro J.
+  symmetry in J. apply length_zero_iff_nil in J. rewrite J. reflexivity.
+  destruct b. inversion J. simpl. rewrite <- IHa. reflexivity.
+  inversion J. reflexivity. rewrite H0. apply J. assumption.
+
+  rewrite combine_length. rewrite H. apply PeanoNat.Nat.min_id.
+Qed.
+
+
 Theorem subsequence_rev {X: Type} :
   forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
 Proof.