Update

src/subsequences.v

@@ -91,6 +91,51 @@ Qed.
 Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
   subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
 Proof.
+  intros l s a. split. intro H. unfold subsequence2 in H.
+  destruct H. destruct H. destruct x. inversion H0.
+  destruct b.
+  exists (x). split. inversion H. reflexivity. simpl in H0.
+  inversion H0. reflexivity. simpl in H0. inversion H.
+  assert (subsequence2 l (a::s)). exists x. split; assumption.
+  apply subsequence2_cons_r with (a := a). assumption.
+
+
+
+
+
+  (* pas mal *)
+  intros l s. generalize l. induction s.
+  intros l0 a. split; intro H. apply subsequence2_nil_r.
+  exists (true :: (map (fun x => false) l0)).
+  split. simpl. rewrite map_length. reflexivity.
+  simpl. induction l0. reflexivity.
+  assert (subsequence2 l0 []). apply subsequence2_nil_r.
+  apply IHl0 in H0. simpl. assumption.
+  intros l0 a0. split. intro H.
+
+
+
+
+  (* pas mal *)
+  intro l. induction l. intros s a. split. intro H.
+  destruct s. apply subsequence2_nil_r.
+  unfold subsequence2 in H. destruct H. destruct H.
+  destruct x. symmetry in H0. apply nil_cons in H0. contradiction H0.
+  destruct b.
+  simpl in H0. destruct x.
+  simpl in H0. inversion H0. inversion H.
+  simpl in H0. destruct x.
+  simpl in H0. inversion H0. inversion H.
+  intro H. destruct s. exists [true]. split; reflexivity.
+  apply subsequence2_nil_cons_r in H. contradiction H.
+  intros s a0. split. intro H.
+
+
+
+
+
+
+
 
   assert (forall (l s: list Type) t,
       s = map snd (filter fst (combine t l))