fix ex16.1 and ex16.5

Author: singleheart

ch16/ex1.txt

@@ -11,8 +11,6 @@ Inductive case:
 add (Succ x) (Succ m)
 = {applying add}
 Succ (add x (Succ m))
-= {applying add}
-Succ (add x (Succ m))
 = {induction hypothesis}
 Succ (Succ (add x m))
 = {unapplying add}

ch16/ex5.txt

@@ -20,8 +20,10 @@ xs
 Inductive case:
 take (n+1) (x:xs) ++ drop (n+1) (x:xs)
 = {applying take}
-x : take n xs ++ drop (n+1) (x:xs)
+(x : take n xs) ++ drop (n+1) (x:xs)
 = {applying drop}
-x : take n xs ++ drop n xs
+(x : take n xs) ++ drop n xs
+= {applying ++}
+x : (take n xs ++ drop n xs)
 = {induction hypothesis}
 x : xs