Update
This commit is contained in:
parent
00cf74be9c
commit
24d88f1928
@ -232,7 +232,6 @@ Proof.
|
|||||||
apply length_zero_iff_nil in I. rewrite I. reflexivity.
|
apply length_zero_iff_nil in I. rewrite I. reflexivity.
|
||||||
destruct u. apply O_S in I. contradiction I.
|
destruct u. apply O_S in I. contradiction I.
|
||||||
simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
|
simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
|
||||||
|
|
||||||
rewrite H1. rewrite <- H2; inversion H; reflexivity.
|
rewrite H1. rewrite <- H2; inversion H; reflexivity.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
@ -250,15 +249,11 @@ Proof.
|
|||||||
rewrite J. apply subsequence3_nil_r.
|
rewrite J. apply subsequence3_nil_r.
|
||||||
destruct v. apply subsequence3_nil_r.
|
destruct v. apply subsequence3_nil_r.
|
||||||
destruct w. apply Nat.neq_succ_0 in I. contradiction I.
|
destruct w. apply Nat.neq_succ_0 in I. contradiction I.
|
||||||
destruct a. exists nil. exists w.
|
destruct a. exists nil. exists w. inversion J.
|
||||||
inversion J. apply IHu in H3.
|
apply IHu in H3. split; inversion J; try rewrite <- H5; easy.
|
||||||
split. reflexivity. inversion J. rewrite <- H5. assumption.
|
inversion I. reflexivity.
|
||||||
inversion I. reflexivity. simpl in J.
|
assert (subsequence3 w (x0::v)). apply IHu; inversion I; easy.
|
||||||
|
apply subsequence3_cons_l; assumption.
|
||||||
assert (subsequence3 w (x0::v)). apply IHu.
|
|
||||||
inversion I. reflexivity. assumption.
|
|
||||||
apply subsequence3_cons_l. assumption.
|
|
||||||
|
|
||||||
apply I with (u := x); assumption.
|
apply I with (u := x); assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user