Skip to content

Commit 1824aed

Browse files
negatratoronJefferson Carpenter
andauthored
Extensionality not required for proof of neg any equiv all neg (plfa#1086)
Co-authored-by: Jefferson Carpenter <jefferson@aoeu2code.com>
1 parent 2400b73 commit 1824aed

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/plfa/part1/Lists.lagda.md

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -995,7 +995,6 @@ If so, prove; if not, explain why.
995995
#### Exercise `¬Any≃All¬` (stretch)
996996

997997
Show that the equivalence `¬Any⇔All¬` can be extended to an isomorphism.
998-
You will need to use extensionality.
999998

1000999
```agda
10011000
-- Your code goes here

0 commit comments

Comments
 (0)