drop a superfluous assumption that was found by the find_unused_assms command and tune proof

--- a/src/HOL/List.thy	Fri Oct 20 20:57:55 2017 +0200
+++ b/src/HOL/List.thy	Sat Oct 21 18:11:29 2017 +0200
@@ -4902,9 +4902,8 @@
 by(induction xs arbitrary: x)(auto intro: transpD[OF assms])
 
 lemma sorted_wrt_ConsI:
-  "\<lbrakk> transp P; \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow>
-  sorted_wrt P (x # xs)"
-by (simp add: sorted_wrt_Cons)
+  "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
+by (induction xs rule: sorted_wrt_induct) simp_all
 
 lemma sorted_wrt_append:
 assumes "transp P"