216 apply(simp add: finite_supp)

   216 apply(simp add: finite_supp)

   217 apply(simp add: finite_supp)

   217 apply(simp add: finite_supp)

   218 apply(simp add: Abs_fresh_star)

   218 apply(simp add: Abs_fresh_star)

   219 done

   219 done

   220 

   220 

   221 

   224 

   222 lemma strong_exhaust2:

   225 lemma strong_exhaust2:

   223   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 

   226   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 

   224   shows "P"

   227   shows "P"

   225 apply(rule_tac y="as" in foo.exhaust(2))

   228 apply(rule_tac y="as" in foo.exhaust(2))