[PostScript]
InsertGenerated (E, C): trait % C's contain finitely many E's introduces empty: -> C insert: E, C -> C asserts C generated by empty, insert