diff options
| -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') |