fix notes again (#974)

Author: jsiek

src/plfa/part2/Confluence.lagda.md

@@ -607,13 +607,9 @@ confluence L↠M₁ L↠M₂
 
 ## Notes
 
-This mechanized proof of confluence is based on several sources. The
-`subst-par` lemma is the "strong substitutivity" lemma of
-@Schafer:2015. The proofs of `par-triangle`, `strip`,
-and `par-confluence` are based on the notion of complete development
-by @Takahashi:1995 and the technical report by @Pfenning:1992 about the
-Church-Rosser theorem. In addition, we consulted Nipkow and
-Berghofer's mechanization in Isabelle, which is based on an earlier
+This mechanized proof of confluence is loosely based on several
+sources including @Schafer:2015, @Takahashi:1995, @Pfenning:1992, and
+Nipkow and Berghofer's mechanization in Isabelle, which is based on a
 paper by @Nipkow:1996.
 
 ## Unicode