I would like to ask if there is any good list of graph properties that one can express in the MSO2 (i.e., using quantification over sets of edges) but provably not in MSO1 (i.e., using quantification over sets of vertices only). I know that this should be Hamilton path but I think that there has to be plenty such examples. Ideal are those that are suitable as exercises for non-expressibility results using EF games.