[STATEMENT]
lemma abs_pred_stermI[intro]:
  assumes "\<And>cs. (\<And>pat t. (pat, t) \<in> set cs \<Longrightarrow> P t) \<Longrightarrow> P (Sabs cs)"
  shows "abs_pred P t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_pred P t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<And>pat t. (pat, t) \<in> set ?cs \<Longrightarrow> P t) \<Longrightarrow> P (Sabs ?cs)

goal (1 subgoal):
 1. abs_pred P t
[PROOF STEP]
unfolding abs_pred_sterm_def
[PROOF STATE]
proof (prove)
using this:
(\<And>pat t. (pat, t) \<in> set ?cs \<Longrightarrow> P t) \<Longrightarrow> P (Sabs ?cs)

goal (1 subgoal):
 1. \<forall>cs. t = Sabs cs \<longrightarrow> (\<forall>pat t. (pat, t) \<in> set cs \<longrightarrow> P t) \<longrightarrow> P t
[PROOF STEP]
by auto