[STATEMENT]
lemma AbstrLevels_S10_A71:
  assumes "sS10 \<in> AbstrLevel i"
  shows "sA71 \<notin> AbstrLevel i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sA71 \<notin> AbstrLevel i
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sA71 \<notin> AbstrLevel i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sS10 \<in> AbstrLevel i

goal (1 subgoal):
 1. sA71 \<notin> AbstrLevel i
[PROOF STEP]
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)