diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-11-07 13:25:34 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-11-07 13:27:36 -0500 |
| commit | b953c040b36f34b480759f0c4cd275eff4d1efa5 (patch) | |
| tree | dd2f6e1b0ac2613ce1f532376daee0ab11a87f54 /src/Util | |
| parent | 9e767c9bfe4158215e4efaa1a4cc1744bb0b2b58 (diff) | |
ModularBaseSystem: prove some admits in mase system extension
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil.v | 5 |
1 files changed, 3 insertions, 2 deletions
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) |