From 3e03d1ee0315cbded81eb145fb9698407ce8cb3a Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Sun, 29 Aug 2021 10:29:46 +0100 Subject: [PATCH] Update Lists.lagda.md --- src/plfa/part1/Lists.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 8dcc3541..16a7b380 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -990,7 +990,7 @@ You will need to use extensionality. #### Exercise `All-∀` (practice) -Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`. +Show that `All P xs` is isomorphic to `∀ x → x ∈ xs → P x`. ``` -- You code goes here