From eae2f16659e7f3bded205f7870835eaa705eded6 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Mon, 27 Jan 2020 16:18:00 -0500 Subject: [PATCH] fix a typo --- src/plfa/part1/Quantifiers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index ce377716..bf412066 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -465,7 +465,7 @@ And to establish the following properties: Using the above, establish that there is an isomorphism between `ℕ` and `∃[ b ](Can b)`. -We recommend proving following lemmas which show that, for a given +We recommend proving the following lemmas which show that, for a given binary number `b`, there is only one proof of `One b` and similarly for `Can b`.