pi and rho determine an atom of concept T uniquely, you can write:<label> is the name of the rule. It can be a single word or a string (enclosed by double brackets). It is followed by a colon (:) to distinguish the label from the concept that follows.<Concept> is the name of the Concept for atoms of which the rule specifies an identity<Concept>. This is enforced by the type system.eis both univalent and total, e<>e~ equals e;e~, and the rule is equivalent to:e is univalent but not total, you should use the IDENT statement (or the rule that it implements), because that also works when an e is not populated.