--- a/NEWS Mon Dec 19 12:00:15 2022 +0100
+++ b/NEWS Mon Dec 19 12:00:56 2022 +0100
@@ -124,6 +124,7 @@
asym_on_lex_prod[simp]
irrefl_lex_prod[simp]
irrefl_on_lex_prod[simp]
+ refl_lex_prod[simp]
sym_lex_prod[simp]
sym_on_lex_prod[simp]
wfP_if_convertible_to_nat