From 5bb615a335a9c64e31fa5e9ae5d3a41a731c07a8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Mar 2017 14:36:28 -0400 Subject: generalize In_firstn_skipn_split --- src/Util/ListUtil.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/ListUtil.v') 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') -- cgit v1.2.3