diff --git a/src/Solutions/Eq.idr b/src/Solutions/Eq.idr
index 0e4c22a3..6671268c 100644
--- a/src/Solutions/Eq.idr
+++ b/src/Solutions/Eq.idr
@@ -57,7 +57,7 @@ sctCong f SameCT = Refl
 
 natEq : (n1,n2 : Nat) -> Maybe (n1 = n2)
 natEq 0     0     = Just Refl
-natEq (S k) (S j) = cong S <$> natEq k j
+natEq (S k) (S j) = (\x => cong S x) <$> natEq k j
 natEq (S k) 0     = Nothing
 natEq 0     (S _) = Nothing
 
@@ -237,7 +237,7 @@ ctNatInjective Float   Float   Refl = Refl
 DecEq ColType where
   decEq c1 c2 = case decEq (ctNat c1) (ctNat c2) of
     Yes prf    => Yes $ ctNatInjective c1 c2 prf
-    No  contra => No $ contra . cong ctNat
+    No  contra => No $ \x => contra $ cong ctNat x
 
 --------------------------------------------------------------------------------
 --          Rewrite Rules
diff --git a/src/Tutorial/Eq.md b/src/Tutorial/Eq.md
index 8b790737..33aa0f4c 100644
--- a/src/Tutorial/Eq.md
+++ b/src/Tutorial/Eq.md
@@ -651,7 +651,7 @@ Actually, this is just a specialized version of the contraposition of
 
 ```idris
 contraCong : {0 f : _} -> Not (f a = f b) -> Not (a = b)
-contraCong fun = fun . cong f
+contraCong fun x = fun $ cong f x
 ```
 
 ### Interface `Uninhabited`
diff --git a/src/Tutorial/Prim.md b/src/Tutorial/Prim.md
index 4931391f..8b027ab3 100644
--- a/src/Tutorial/Prim.md
+++ b/src/Tutorial/Prim.md
@@ -1025,7 +1025,7 @@ utility functions:
 
 ```idris
 data IsYes0 : (d : Dec0 prop) -> Type where
-  ItIsYes0 : IsYes0 (Yes0 prf)
+  ItIsYes0 : {0 prf : _} -> IsYes0 (Yes0 prf)
 
 0 fromYes0 : (d : Dec0 prop) -> (0 prf : IsYes0 d) => prop
 fromYes0 (Yes0 x) = x