--- a/src/Equality.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/Equality.v	Sun Jan 20 15:16:29 2019 -0500
@@ -214,7 +214,7 @@
     end.
 End fhlist.
 
-Implicit Arguments fhget [A B elm ls].
+Arguments fhget [A B elm ls].
 
 (* begin hide *)
 (* begin thide *)
@@ -235,7 +235,7 @@
       | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
     end.
 
-  Implicit Arguments fhmap [ls].
+  Arguments fhmap [ls].
 
   (* begin hide *)
   (* begin thide *)
@@ -496,7 +496,7 @@
       | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
     end.
 
-  Implicit Arguments fhapp [ls1 ls2].
+  Arguments fhapp [ls1 ls2].
 
   (* EX: Prove that fhapp is associative. *)
 (* begin thide *)
@@ -676,7 +676,7 @@
 (* end thide *)
 End fhapp.
 
-Implicit Arguments fhapp [A B ls1 ls2].
+Arguments fhapp [A B ls1 ls2].
 
 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics.  The next section explores an alternative that leads to simpler developments in some cases. *)