diff -r 1d8e914e04d6 -r 572ab9e64e18 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/Library/More_List.thy	Wed Feb 05 20:17:00 2020 +0000
@@ -378,5 +378,18 @@
     by simp
 qed
 
+lemma nth_default_map2:
+  \<open>nth_default d (map2 f xs ys) n = f (nth_default d1 xs n) (nth_default d2 ys n)\<close>
+    if \<open>length xs = length ys\<close> and \<open>f d1 d2 = d\<close> for bs cs
+using that proof (induction xs ys arbitrary: n rule: list_induct2)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons x xs y ys)
+  then show ?case
+    by (cases n) simp_all
+qed
+
 end