From e42aa017dac06a10b319e00be04681393c22b8e4 Mon Sep 17 00:00:00 2001 From: Jonathan Prieto-Cubides Date: Fri, 6 Jul 2018 00:11:44 +0200 Subject: [PATCH] [ Induction ] Fix typo of of typo --- src/plfa/Induction.lagda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/Induction.lagda b/src/plfa/Induction.lagda index a678a0fc..c450df23 100644 --- a/src/plfa/Induction.lagda +++ b/src/plfa/Induction.lagda @@ -314,7 +314,7 @@ For the base case, we must show: zero + zero ≡ zero -Simplifying with the base case of of addition, this is straightforward. +Simplifying with the base case of addition, this is straightforward. For the inductive case, we must show: @@ -385,7 +385,7 @@ For the base case, we must show: zero + suc n ≡ suc (zero + n) -Simplifying with the base case of of addition, this is straightforward. +Simplifying with the base case of addition, this is straightforward. For the inductive case, we must show: