Myhill_1.thy
2011-02-11 urbanc slightly streamlined the proof
less more (0) -10 -1 tip