From 6be6e0a4b9828512fda0d3d81cf56fdff808af27 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 11:28:07 -0700 Subject: Fix some typos in the previous commit --- src/Util/ListUtil.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index caeaefdb2..da02faa22 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -873,8 +873,8 @@ Proof. erewrite nth_error_value_eq_nth_default by eassumption; reflexivity. Qed. -Lemma nth_default_in_bounds : forall {T} n us (d d' : T), (n < length us)%nat -> - nth_default d us n = nth_default d us n. +Lemma nth_default_in_bounds : forall {T} (d' d : T) n us, (n < length us)%nat -> + nth_default d us n = nth_default d' us n. Proof. intros; erewrite !nth_default_nth_dep; reflexivity. Grab Existential Variables. -- cgit v1.2.3