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 | |
parent | 2c813835518ce6c67c524355977ea22b77438e40 (diff) |
generalize In_firstn_skipn_split
-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') |