theory Simproc_Fail
imports Main
begin

notepad
begin
  have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp
  hence True apply simp sorry
end

end