achieved full automation with metis in Isabelle; some lemmata were introduced for this