[STATEMENT]
lemma last_fst_esp: 
 "fst(((Some a,s)#xs)!(length xs))=None \<Longrightarrow> fst(xs!(length xs - (Suc 0)))=None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (((Some a, s) # xs) ! length xs) = None \<Longrightarrow> fst (xs ! (length xs - Suc 0)) = None
[PROOF STEP]
apply(erule last_fst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Some a, s) \<noteq> None
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done