diff options
author | jadep <jade.philipoom@gmail.com> | 2018-09-18 12:00:37 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-12-21 10:22:41 -0500 |
commit | 943d76f97fcbb02ca5d417266ad9dcd7a9561a73 (patch) | |
tree | 35113960fab7845b39314544f974220307cbcd33 /src/Util | |
parent | 9883e4e7a60ba7d1e1487f7a4501363bd3958fde (diff) |
prove [eval_conditional_sub]
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/ListUtil.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 9f6658c42..cb11eca3b 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1297,6 +1297,7 @@ Proof. revert k a; induction b as [|? IHb], k; simpl; try reflexivity. intros; rewrite IHb; reflexivity. Qed. +Hint Rewrite @firstn_seq : push_firstn. Lemma skipn_seq k a b : skipn k (seq a b) = seq (k + a) (b - k). |