[STATEMENT]
lemma delete_edges_set_nodes: "set (nodesL (delete_edges G E)) = set (nodesL G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (nodesL (FiniteListGraph.delete_edges G E)) = set (nodesL G)
[PROOF STEP]
by (induction E arbitrary: G) (auto simp: delete_edge_set_nodes)