diff options
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 36d8a3ad3..dd1e6a5c5 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -258,13 +258,13 @@ Proof. destruct (lt_dec n (length xs)); auto. Qed. -Lemma combine_truncate_r : forall {A} (xs ys : list A), +Lemma combine_truncate_r : forall {A B} (xs : list A) (ys : list B), combine xs ys = combine xs (firstn (length xs) ys). Proof. induction xs; destruct ys; boring. Qed. -Lemma combine_truncate_l : forall {A} (xs ys : list A), +Lemma combine_truncate_l : forall {A B} (xs : list A) (ys : list B), combine xs ys = combine (firstn (length ys) xs) ys. Proof. induction xs; destruct ys; boring. |