issue-1916-spec.k: Describe what is being tested

Author: ttuegel

test/check-implication/issue-1916-spec.k

@@ -5,5 +5,8 @@ endmodule
 module ISSUE-1916-SPEC
   import VERIFICATION
 
+  // Proving this claim requires that the right-hand side is simplified using
+  // the conditions from the left-hand side.
+  //
   rule <k> begin => end </k> requires isFun(X) ensures true #And #Ceil(fun(X))
 endmodule