@@ -1028,6 +1028,9 @@ eqCon = sUN "refl"
10281028eqDoc = parseDocstring . T.pack $
10291029 "The propositional equality type. A proof that `x` = `y`." ++
10301030 "\n\n" ++
1031+ "To use such a proof, pattern-match on it, and the two equal things will " ++
1032+ "then need to be the _same_ pattern." ++
1033+ "\n\n" ++
10311034 "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++
10321035 "is possible to state equalities between values of potentially different " ++
10331036 "types. This is sometimes referred to in the literature as \"John Major\" " ++