inductive2 = Gfp + Sum + Prod + consts Part :: "['b => 'a, 'a set] => 'b set" defs Part_def "Part f S == {x. f x : S}" end