diff --git a/.gitignore b/.gitignore
index 2d7777f3..3a8c59f5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,8 +21,11 @@ Gemfile.lock
 *.spl
 *.synctex.gz
 
-## EPUB files
-*.epub
+## Lua files
+lua_modules/
 
 ## Emacs files
 auto/
+
+## Misc build files
+out/
diff --git a/.travis.yml b/.travis.yml
index 7269268f..c6144bbb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -8,7 +8,6 @@ cache:
   bundler: true
   timeout: 1500
   directories:
-  - out/
   - $HOME/.stack
   - $HOME/.agda
   - $HOME/.local
@@ -20,6 +19,7 @@ cache:
 addons:
   apt:
     packages:
+      - epubcheck
       - libgmp-dev
       - libicu-dev
 
@@ -28,22 +28,24 @@ env:
   - SH=bash
 
 before_install:
-# Download and unpack the stack executable
+# Install Stack:
 - mkdir -p ~/.local/bin
 - export PATH=$HOME/.local/bin:$PATH
 - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
-# Download and install agda, agda-stdlib, and agda2html
+# Install Pandoc:
+- travis_retry curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $HOME/pandoc.deb && sudo dpkg -i $HOME/pandoc.deb
+# Install agda, agda-stdlib, and agda2html:
 - make travis-setup
 
 script:
-- travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python
 - agda --version
 - acknowledgements --version
 - pandoc --version
-- make test-offline # disable to only build cache
+- acknowledgements -i _config.yml >> _config.yml
+- make test-offline # build and test website
+- make epubcheck # build and test EPUB
 
 before_deploy:
-- acknowledgements -i _config.yml >> _config.yml
 - make clean
 - rm -rf hs/ extra/ depr/ papers/ slides/ .bundle/ vendor/ *.agdai *.agda-lib *.lagda.md Guardfile Gemfile Gemfile.lock Makefile highlight.sh .gitignore .travis.yml
 
diff --git a/Gemfile b/Gemfile
index 1eac9d04..4ae04980 100644
--- a/Gemfile
+++ b/Gemfile
@@ -9,3 +9,8 @@ group :development do
   gem 'guard-shell'
   gem 'html-proofer'
 end
+
+group :epub do
+  gem 'safe_yaml'
+  gem 'liquid'
+end
diff --git a/Makefile b/Makefile
index 88c544fd..c57666b0 100644
--- a/Makefile
+++ b/Makefile
@@ -1,9 +1,16 @@
 SHELL := /usr/bin/env bash
-AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
-AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
-LUA := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
-MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
+AGDA_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
+AGDAI_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
+MARKDOWN_FILES := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA_FILES))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
+PANDOC := pandoc
+EPUBCHECK := epubcheck
+RUBY := ruby
+GEM := $(RUBY) -S gem
+BUNDLE := $(RUBY) -S bundle
+JEKYLL := $(BUNDLE) exec jekyll
+HTMLPROOFER := $(BUNDLE) exec htmlproofer
+LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
 
 ifeq ($(AGDA_STDLIB_VERSION),)
 AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/
@@ -13,24 +20,20 @@ endif
 
 
 # Build PLFA and test hyperlinks
-test: build epub
-	ruby -S bundle exec htmlproofer '_site'
+test: build
+	$(HTMLPROOFER) '_site'
 
 
 # Build PLFA and test hyperlinks offline
 test-offline: build
-	ruby -S bundle exec htmlproofer '_site' --disable-external
+	$(HTMLPROOFER) '_site' --disable-external
 
 
 # Build PLFA and test hyperlinks for stable
-test-stable-offline: $(MARKDOWN)
-	ruby -S bundle exec jekyll clean
-	ruby -S bundle exec jekyll build --destination '_site/stable' --baseurl '/stable'
-	ruby -S bundle exec htmlproofer '_site' --disable-external
-
-
-statistics:
-	hs/agda-count
+test-stable-offline: $(MARKDOWN_FILES)
+	$(JEKYLL) clean
+	$(JEKYLL) build --destination '_site/stable' --baseurl '/stable'
+	$(HTMLPROOFER) '_site' --disable-external
 
 
 out/:
@@ -49,19 +52,24 @@ out/:
 #       sections are displayed to users. Some readers may be slow if the chapter
 #       files are too large, so for large documents with few level-1 headings, one
 #       might want to use a chapter level of 2 or 3."
-#
-#TODO: embedded fonts not working (path problem?)
 
-epub: out/plfa.epub
+epub: out/epub/plfa.epub
 
-out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css
-	pandoc --strip-comments \
+epubcheck: out/epub/plfa.epub
+	$(EPUBCHECK) out/epub/plfa.epub
+
+out/epub/:
+	mkdir -p out/epub/
+
+out/epub/plfa.epub: out/epub/ | $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epub/acknowledgements.md
+	$(PANDOC) --strip-comments \
 		--css=epub/main.css \
 		--epub-embed-font='assets/fonts/mononoki.woff' \
 		--epub-embed-font='assets/fonts/FreeMono.woff' \
 		--epub-embed-font='assets/fonts/DejaVuSansMono.woff' \
 		--lua-filter epub/include-files.lua \
 		--lua-filter epub/rewrite-links.lua \
+		--lua-filter epub/rewrite-html-ul.lua \
 		--lua-filter epub/default-code-class.lua -M default-code-class=agda \
 		--standalone \
 		--fail-if-warnings \
@@ -70,7 +78,10 @@ out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css
 		-o "$@" \
 		epub/index.md
 
+out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
+	 $(BUNDLE) exec ruby epub/render-liquid-template.rb _config.yml $< $@
 
+.phony: epub epubcheck
 
 
 # Convert literal Agda to Markdown
@@ -89,17 +100,17 @@ else
 endif
 endef
 
-$(foreach agda,$(AGDA),$(eval $(call AGDA_template,$(agda))))
+$(foreach agda,$(AGDA_FILES),$(eval $(call AGDA_template,$(agda))))
 
 
 # Start server
 serve:
-	ruby -S bundle exec jekyll serve --incremental
+	$(JEKYLL) serve --incremental
 
 
 # Start background server
 server-start:
-	ruby -S bundle exec jekyll serve --no-watch --detach
+	$(JEKYLL) serve --no-watch --detach
 
 
 # Stop background server
@@ -108,26 +119,26 @@ server-stop:
 
 
 # Build website using jekyll
-build: $(MARKDOWN)
-	ruby -S bundle exec jekyll build
+build: $(MARKDOWN_FILES)
+	$(JEKYLL) build
 
 
 # Build website using jekyll incrementally
-build-incremental: $(MARKDOWN)
-	ruby -S bundle exec jekyll build --incremental
+build-incremental: $(MARKDOWN_FILES)
+	$(JEKYLL) build --incremental
 
 
 # Remove all auxiliary files
 clean:
-	rm -f .agda-stdlib.sed .links-*.sed
-ifneq ($(strip $(AGDAI)),)
-	rm $(AGDAI)
+	rm -f .agda-stdlib.sed .links-*.sed out/epub/acknowledgements.md
+ifneq ($(strip $(AGDAI_FILES)),)
+	rm $(AGDAI_FILES)
 endif
 
 
 # Remove all generated files
 clobber: clean
-	ruby -S bundle exec jekyll clean
+	$(JEKYLL) clean
 	rm -rf out/
 
 .phony: clobber
@@ -135,7 +146,7 @@ clobber: clean
 
 # List all .lagda files
 ls:
-	@echo $(AGDA)
+	@echo $(AGDA_FILES)
 
 .phony: ls
 
@@ -143,10 +154,10 @@ ls:
 # MacOS Setup (install Bundler)
 macos-setup:
 	brew install libxml2
-	ruby -S gem install bundler --no-ri --no-rdoc
-	ruby -S gem install pkg-config --no-ri --no-rdoc -v "~> 1.1"
-	ruby -S bundle config build.nokogiri --use-system-libraries
-	ruby -S bundle install
+	$(GEM) install bundler --no-ri --no-rdoc
+	$(GEM) install pkg-config --no-ri --no-rdoc -v "~> 1.1"
+	$(BUNDLE) config build.nokogiri --use-system-libraries
+	$(BUNDLE) install
 
 .phony: macos-setup
 
@@ -157,33 +168,12 @@ travis-setup:\
 	$(HOME)/.local/bin/acknowledgements\
 	$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
 	$(HOME)/.agda/defaults\
-	$(HOME)/.agda/libraries\
-	/usr/bin/pandoc
+	$(HOME)/.agda/libraries
 
 .phony: travis-setup
 
 
-travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements
-
-$(HOME)/.local/bin/acknowledgements:
-	curl -L https://github.com/plfa/acknowledgements/archive/master.zip -o $(HOME)/acknowledgements-master.zip
-	unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
-	cd $(HOME)/acknowledgements-master;\
-		stack install
-
-# The version of pandoc on Xenial is too old.
-/usr/bin/pandoc:
-	curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $(HOME)/pandoc.deb
-	sudo dpkg -i $(HOME)/pandoc.deb
-
-travis-uninstall-acknowledgements:
-	rm -rf $(HOME)/acknowledgements-master/
-	rm $(HOME)/.local/bin/acknowledgements
-
-travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-reinstall-acknowledgements
-
-.phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements
-
+# Agda
 
 travis-install-agda:\
 	$(HOME)/.local/bin/agda\
@@ -199,7 +189,8 @@ $(HOME)/.agda/libraries:
 	echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries
 
 $(HOME)/.local/bin/agda:
-	curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip -o $(HOME)/agda-$(AGDA_VERSION).zip
+	travis_retry curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip\
+	                  -o $(HOME)/agda-$(AGDA_VERSION).zip
 	unzip -qq $(HOME)/agda-$(AGDA_VERSION).zip -d $(HOME)
 	cd $(HOME)/agda-$(AGDA_VERSION);\
 		stack install --stack-yaml=stack-8.0.2.yaml
@@ -214,10 +205,13 @@ travis-reinstall-agda: travis-uninstall-agda travis-install-agda
 .phony: travis-install-agda travis-uninstall-agda travis-reinstall-agda
 
 
+# Agda Standard Library
+
 travis-install-agda-stdlib: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src
 
 $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src:
-	curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip -o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip
+	travis_retry curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip\
+	                  -o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip
 	unzip -qq $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip -d $(HOME)
 	mkdir -p $(HOME)/.agda
 
@@ -229,3 +223,23 @@ travis-uninstall-agda-stdlib:
 travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib
 
 .phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib epub
+
+
+# Acknowledgements
+
+travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements
+
+$(HOME)/.local/bin/acknowledgements:
+	travis_retry curl -L https://github.com/plfa/acknowledgements/archive/master.zip\
+	                  -o $(HOME)/acknowledgements-master.zip
+	unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
+	cd $(HOME)/acknowledgements-master;\
+		stack install
+
+travis-uninstall-acknowledgements:
+	rm -rf $(HOME)/acknowledgements-master/
+	rm $(HOME)/.local/bin/acknowledgements
+
+travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-reinstall-acknowledgements
+
+.phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements
diff --git a/README.md b/README.md
index abec3ef5..f48d015b 100644
--- a/README.md
+++ b/README.md
@@ -32,6 +32,8 @@ permalink: /GettingStarted/
 [ruby-html-proofer]: https://github.com/gjtorikian/html-proofer
 
 [kramdown]: https://kramdown.gettalong.org/syntax.html
+[pandoc]: https://pandoc.org/installing.html
+[epubcheck]: https://github.com/w3c/epubcheck
 
 
 <!-- Status & Version Badges -->
@@ -172,9 +174,13 @@ You'll see the key sequence of the character in mini buffer.
 
 ## Dependencies for developers
 
-Building PLFA is currently supported on Linux and macOS.
+PLFA is available as both a website and an EPUB e-book,
+both of which can be built on Linux and macOS.
 PLFA is written in literate Agda with [Kramdown Markdown][kramdown].
-The book is built in three stages:
+
+### Building the website
+
+The website version of the book is built in three stages:
 
  1. The `.lagda.md` files are compiled to Markdown using Agda’s highlighter.
     (This requires several POSIX tools, such as `bash`, `sed`, and `grep`.)
@@ -216,3 +222,17 @@ If you simply wish to have a local copy of the book, e.g. for offline reading, b
 bundle install
 bundle exec jekyll serve
 ```
+
+### Building the EPUB
+
+The EPUB version of the book is built using Pandoc. Here's how to build the EPUB:
+
+1. Install a recent version of Pandoc, [available here][pandoc].
+   We recommend their official installer (on the linked page),
+   which is much faster than compiling Pandoc from source with Haskell Stack.
+
+2. Build the EPUB by running:
+   ```bash
+   make epub
+   ```
+   The EPUB is written to `out/epub/plfa.epub`.
diff --git a/_config.yml b/_config.yml
index 9cd89930..f0a4ac89 100644
--- a/_config.yml
+++ b/_config.yml
@@ -67,3 +67,4 @@ exclude:
   - "Gemfile"
   - "Gemfile.lock"
   - "highlight.sh"
+  - "out/epub/acknowledgements.md"
diff --git a/_posts/2020-06-02-plfa-as-epub.md b/_posts/2020-06-02-plfa-as-epub.md
new file mode 100644
index 00000000..1fff7fed
--- /dev/null
+++ b/_posts/2020-06-02-plfa-as-epub.md
@@ -0,0 +1,10 @@
+---
+layout : post
+title  : "PLFA as EPUB"
+---
+
+It has been just over a year and a half since this feature was first requested in [#112][issue112]… Thanks to hard work by [Michael Reed][mreed20], and a little elbow grease on our part, it is finally here! [An EPUB version of PLFA!][epub]
+
+[epub]: https://plfa.github.io/out/epub/plfa.epub
+[issue112]: https://github.com/plfa/plfa.github.io/issues/112
+[mreed20]: https://github.com/mreed20
diff --git a/epub/index.md b/epub/index.md
index 1124e8d0..6976f2fe 100644
--- a/epub/index.md
+++ b/epub/index.md
@@ -65,9 +65,9 @@ src/plfa/part2/Substitution.lagda.md
 # Backmatter
 
 ``` {.include shift-heading-level-by=1}
-src/plfa/acknowledgements.md
+out/epub/acknowledgements.md
 src/plfa/Fonts.lagda.md
 src/plfa/statistics.md
 ```
 
-<!-- TODO: include the rest of the stuff on https://plfa.github.io/ -->
\ No newline at end of file
+<!-- TODO: include the rest of the stuff on https://plfa.github.io/ -->
diff --git a/epub/render-liquid-template.rb b/epub/render-liquid-template.rb
new file mode 100644
index 00000000..927b25b5
--- /dev/null
+++ b/epub/render-liquid-template.rb
@@ -0,0 +1,19 @@
+#!/usr/bin/env ruby
+require 'yaml'
+require 'liquid'
+
+unless ARGV.length == 3
+  abort "Usage: render-liquid-template.rb [yaml_file] [markdown_in_file] [markdown_out_file]"
+end
+
+yaml_file, markdown_file_in, markdown_file_out = ARGV
+
+[yaml_file, markdown_file_in].each do |file|
+  unless File.file? file
+    abort "File does not exist: '%s'" % [file]
+  end
+end
+
+metadata = { 'site' => (YAML.load (File.read yaml_file)) }
+template = Liquid::Template.parse (File.read markdown_file_in)
+File.write markdown_file_out, (template.render metadata)
diff --git a/epub/rewrite-html-ul.lua b/epub/rewrite-html-ul.lua
new file mode 100644
index 00000000..5a83375a
--- /dev/null
+++ b/epub/rewrite-html-ul.lua
@@ -0,0 +1,5 @@
+-- Transforms '<ul class={something}>' into '<ul>'.
+function RawBlock (el)
+    el.text = el.text:gsub('%s*<%s*ul%s*class=%s*"?[%w-]+"?%s*>%s*', '<ul>')
+    return el
+end
\ No newline at end of file
diff --git a/highlight.sh b/highlight.sh
index e6caefb9..29aa5b1f 100755
--- a/highlight.sh
+++ b/highlight.sh
@@ -110,7 +110,7 @@ for INCLUDE_PATH in "$@"; do
             find "$INCLUDE_PATH" -name "*.lagda.md" -print0 | while read -d $'\0' AGDA_MODULE_SRC; do
                 AGDA_MODULE_OUT="$(out_path "$AGDA_MODULE_SRC")"
                 AGDA_MODULE_HTML="$(basename "$(html_path "$AGDA_MODULE_SRC" "$HTML_DIR")" .md).html"
-                echo "s|$AGDA_MODULE_HTML|{% endraw %}{{ site.baseurl }}{% link $AGDA_MODULE_OUT %}{% raw %}|;" >> "$LOCAL_LINKS_SED"
+                echo "s|$AGDA_MODULE_HTML|{% endraw %}{{ site.baseurl }}{% link $AGDA_MODULE_OUT %}{% raw %}|g;" >> "$LOCAL_LINKS_SED"
             done
         fi
 
diff --git a/src/plfa/acknowledgements.md b/src/plfa/acknowledgements.md
index f3fc8bf6..6df83e23 100644
--- a/src/plfa/acknowledgements.md
+++ b/src/plfa/acknowledgements.md
@@ -7,12 +7,14 @@ next      : /Fonts/
 ---
 
 Thank you to:
-  * The inventors of Agda, for a new playground.
-  * The authors of Software Foundations, for inspiration.
+
+* The inventors of Agda, for a new playground.
+* The authors of Software Foundations, for inspiration.
 
 
 A special thank you, for inventing ideas on which
 this book is based, and for hand-holding:
+
 <ul class="list-of-contributors">
 <li>Andreas Abel</li>
 <li>Catarina Coquand</li>
@@ -25,32 +27,34 @@ this book is based, and for hand-holding:
 <li>Ulf Norell</li>
 </ul>
 
-{%- if site.contributors or site.extra_contributors -%}
+{% if site.contributors or site.extra_contributors %}
 For pull requests big and small, and for answering questions on the Agda mailing list:
+
 <ul class="list-of-contributors">
-{%- for contributor in site.contributors -%}
+{% for contributor in site.contributors %}
   <li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.name }}</a></li>
-{%- endfor -%}
-{%- for contributor in site.extra_contributors -%}
-  {%- if contributor.name and contributor.github_username -%}
+{% endfor %}
+{% for contributor in site.extra_contributors %}
+  {% if contributor.name and contributor.github_username %}
   <li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.name }}</a></li>
-  {%- else -%}
-  {%- if contributor.name -%}
+  {% else %}
+  {% if contributor.name %}
   <li>{{ contributor.name }}</li>
-  {%- endif -%}
-  {%- if contributor.github_username -%}
+  {% endif %}
+  {% if contributor.github_username %}
   <li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.github_username }}</a></li>
-  {%- endif -%}
-  {%- endif -%}
-{%- endfor -%}
+  {% endif %}
+  {% endif %}
+{% endfor %}
 <li>[Your name goes here]</li>
 </ul>
-{%- else -%}
-{%- endif -%}
+{% else %}
+{% endif %}
 
 
 For support:
-  * EPSRC Programme Grant EP/K034413/1
-  * NSF Grant No. 1814460
-  * Foundation Sciences Mathematiques de Paris (FSMP)
-    Distinguised Professor Fellowship
+
+* EPSRC Programme Grant EP/K034413/1
+* NSF Grant No. 1814460
+* Foundation Sciences Mathematiques de Paris (FSMP)
+  Distinguised Professor Fellowship
\ No newline at end of file
diff --git a/src/plfa/dedication.md b/src/plfa/dedication.md
index 585dc757..ccbe0ff4 100644
--- a/src/plfa/dedication.md
+++ b/src/plfa/dedication.md
@@ -6,8 +6,17 @@ next      : /Preface/
 ---
 
 <p style="text-align:center;">
-  <p style="font-size:1.5em">de Philip, para Wanda</p>
-  <p style="font-size:1.17em">amor da minha vida</p>
-  <p style="font-size:1em">knock knock knock</p>
-  <p style="font-size:1em">...</p>
+  <span style="font-size:1.5em">de Philip, para Wanda</span>
+</p>
+
+<p style="text-align:center;">
+  <span style="font-size:1.17em">amor da minha vida</span>
+</p>
+
+<p style="text-align:center;">
+  <span style="font-size:1em">knock knock knock</span>
+</p>
+
+<p style="text-align:center;">
+  <span style="font-size:1em">...</span>
 </p>
diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md
index 0e621d44..fbdca82f 100644
--- a/src/plfa/part1/Relations.lagda.md
+++ b/src/plfa/part1/Relations.lagda.md
@@ -280,8 +280,8 @@ hold, then `m ≤ p` holds.  Again, `m`, `n`, and `p` are implicit:
 ≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)
 ```
 Here the proof is by induction on the _evidence_ that `m ≤ n`.  In the
-base case, the first inequality holds by `z≤n` and must show `zero ≤
-p`, which follows immediately by `z≤n`.  In this case, the fact that
+base case, the first inequality holds by `z≤n` and must show `zero ≤ p`,
+which follows immediately by `z≤n`.  In this case, the fact that
 `n ≤ p` is irrelevant, and we write `_` as the pattern to indicate
 that the corresponding evidence is unused.