From 0715c86ff4deaf7cc1a821020a0639d5464b5afb Mon Sep 17 00:00:00 2001
From: Daniel Selsam <dselsam@users.noreply.github.com>
Date: Fri, 2 Oct 2015 10:17:38 -0700
Subject: [PATCH] fix(library/export): closes #841

---
 doc/export_format.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/export_format.md b/doc/export_format.md
index a8042b920f..f8d61bfaf7 100644
--- a/doc/export_format.md
+++ b/doc/export_format.md
@@ -112,8 +112,8 @@ Here is the sequence of commands for creating the term `fun {A : Type.{1}} (a :
 1 #US 0
 1 #ES 1
 2 #EV 0
-3 #EL #BD 2 2
-4 #EL #BI 1 3
+3 #EL #BD 2 2 2
+4 #EL #BI 1 1 3
 ```
 Now, assume the environment contains the following constant declarations:
 `nat : Type.{1}`, `nat.zero : nat`, `nat.succ : nat -> nat`, and `vector.{l} : Type.{l} -> nat -> Type.{max 1 l}`.