src/HOL/List.thy

--- a/src/HOL/List.thy	Wed May 20 08:33:53 2020 +0200
+++ b/src/HOL/List.thy	Wed May 20 15:00:25 2020 +0100
@@ -6460,6 +6460,10 @@
   then show ?thesis by (intro that [of "length us"]) auto
 qed
 
+lemma irrefl_lex: "irrefl r \<Longrightarrow> irrefl (lex r)"
+  by (meson irrefl_def lex_take_index)
+
+
 
 subsubsection \<open>Lexicographic Ordering\<close>