src/Doc/Datatypes/Datatypes.thy

       unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
       by (blast intro: ignore_Inl_equivp)
 
     lift_bnf 'a myoption (*<*)[wits: "Inl undefined :: 'a + 'a"](*>*)
 
-    proof (intro rel_funI)
-      fix f g :: "'a \<Rightarrow> 'b" and x y :: "'a + 'a"
-      assume "f = g" "ignore_Inl x y"
-      then show "ignore_Inl (map_sum f f x) (map_sum g g y)"
-        by (cases x; cases y) auto
-    next
+    proof -
       fix P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
       assume "P OO Q \<noteq> bot"
       then show "rel_sum P P OO ignore_Inl OO rel_sum Q Q
          \<le> ignore_Inl OO rel_sum (P OO Q) (P OO Q) OO ignore_Inl"
         by (fastforce(*<*) elim!: ignore_Inl.cases simp add: relcompp_apply fun_eq_iff rel_sum.simps(*>*))