Update
This commit is contained in:
parent
d80ca6b8bb
commit
d1927fca71
@ -283,7 +283,7 @@ Proof.
|
|||||||
assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl. destruct H0.
|
assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl. destruct H0.
|
||||||
|
|
||||||
rewrite <- subsequence2_cons_eq with (a := a) in s0.
|
rewrite <- subsequence2_cons_eq with (a := a) in s0.
|
||||||
apply subsequence2_cons_r in s0. left. assumption.
|
apply subsequence2_cons_r in s0. left; assumption.
|
||||||
|
|
||||||
destruct s. left. apply subsequence2_nil_r.
|
destruct s. left. apply subsequence2_nil_r.
|
||||||
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
|
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
|
||||||
|
Loading…
Reference in New Issue
Block a user