[...] > Can you tell me how > I should do in the proof of the lemma continues to Isabelle runs through > here? It was already pointed out that such questions are off-topic for this list. Please repost to isabelle-users at cl.cam.ac.uk ! Alex