From 8ef93f790bdc17c487972b0054e0369d55861a6f Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Wed, 25 Mar 2020 15:25:59 -0400 Subject: [PATCH] fixed hint --- src/plfa/part1/Relations.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 77ffbcfc..0e621d44 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -791,8 +791,8 @@ and back is the identity: to (from b) ≡ b (Hint: For each of these, you may first need to prove related -properties of `One`. Also, you may need to prove that `1` is -less or equal to the result of `from b`.) +properties of `One`. Also, you may need to prove that +if `One b` then `1` is less or equal to the result of `from b`.) ``` -- Your code goes here