From b953c040b36f34b480759f0c4cd275eff4d1efa5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 7 Nov 2015 13:25:34 -0500 Subject: ModularBaseSystem: prove some admits in mase system extension --- src/Util/ListUtil.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/Util') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index c5c1eba4a..229fb7488 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -167,8 +167,9 @@ Lemma nth_error_app : forall {T} n (xs ys:list T), nth_error (xs ++ ys) n = then nth_error xs n else nth_error ys (n - length xs). Proof. - induction n; destruct xs; destruct ys; nth_tac. -Admitted. + induction n; destruct xs; nth_tac; + rewrite IHn; destruct (lt_dec n (length xs)); trivial; omega. +Qed. Lemma nth_default_app : forall {T} n x (xs ys:list T), nth_default x (xs ++ ys) n = if lt_dec n (length xs) -- cgit v1.2.3