Update
This commit is contained in:
parent
43d97734b2
commit
d80ca6b8bb
|
@ -294,10 +294,8 @@ Proof.
|
||||||
destruct I. destruct H0. destruct x0.
|
destruct I. destruct H0. destruct x0.
|
||||||
symmetry in H1. apply nil_cons in H1. contradiction H1.
|
symmetry in H1. apply nil_cons in H1. contradiction H1.
|
||||||
destruct b.
|
destruct b.
|
||||||
inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.
|
inversion H1. rewrite H3 in n0. easy.
|
||||||
|
apply n. exists x0; split; inversion H0; easy.
|
||||||
assert (subsequence2 l (x::s)). exists x0. split; inversion H0; easy.
|
|
||||||
apply n in H2. contradiction H2.
|
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user