Update
This commit is contained in:
parent
bcc5139b6f
commit
2eb631de5e
@ -584,6 +584,24 @@ Theorem subsequence_map {X Y: Type} :
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem subsequence_incl {X: Type} :
|
||||||
|
forall (u v: list X), subsequence u v -> incl v u.
|
||||||
|
Proof.
|
||||||
|
intros u v. intro H. intro a. intro I.
|
||||||
|
generalize I. generalize H. generalize u.
|
||||||
|
induction v; intros u0; intros J K. inversion K.
|
||||||
|
destruct K. rewrite H0 in J.
|
||||||
|
apply subsequence_eq_def_1 in J.
|
||||||
|
apply subsequence_eq_def_2 in J.
|
||||||
|
destruct J. destruct H1. destruct H1. rewrite H1.
|
||||||
|
|
||||||
|
assert (J: forall (u v : list X) w, In w (u++w::v)).
|
||||||
|
intro u1. induction u1; intros v0 w. left. reflexivity.
|
||||||
|
right. apply IHu1. apply J. apply IHv.
|
||||||
|
|
||||||
|
apply subsequence_cons_r in H. assumption. assumption.
|
||||||
|
apply subsequence_cons_r in J. assumption. assumption.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
(** * Tests
|
(** * Tests
|
||||||
|
Loading…
Reference in New Issue
Block a user