diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-19 14:36:28 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-19 14:36:28 -0400 |
| commit | 5bb615a335a9c64e31fa5e9ae5d3a41a731c07a8 (patch) | |
| tree | 2c8513b3c8bf3433ae51533152e9de54927b025e /src/Util/ListUtil.v | |
| parent | 2c813835518ce6c67c524355977ea22b77438e40 (diff) | |
generalize In_firstn_skipn_split
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 9c5514ccc..5b43e1e05 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1153,9 +1153,9 @@ Proof. Qed. Lemma In_firstn_skipn_split {T} n (x : T) - : forall l, In x l -> In x (firstn n l) \/ In x (skipn n l). + : forall l, In x l <-> In x (firstn n l) \/ In x (skipn n l). Proof. - induction n; destruct l; boring. + split; revert l; induction n; destruct l; boring. match goal with | [ IH : forall l, In ?x l -> _ \/ _, H' : In ?x ?ls |- _ ] => destruct (IH _ H') |