[STATEMENT]
lemma set_nongens_impl: "set (nongens_impl Q) = nongens Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (nongens_impl Q) = nongens Q
[PROOF STEP]
by (auto simp: nongens_def nongens_impl_def set_gen_impl simp flip: List.set_empty)