x_{1} is a value / proof of type / proposition x_{2} under context x_{3} in (type / logical) system x_{4}.

Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: "x_{3 \vdash x}", with x_{4} implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written "x_{3 \vdash x}". x_{1} is most likely to be filled by a li construct, or something that potentially reduces to a mathematical expression. Quoted arguments should be dereferenced with la'e or similar. x_{1} can be filled by zi'o, which means that the proposition is unprovable. x_{2} can be filled by a set of which the x_{1} value is a member. It may be convenient to interpret lo'i as the gadri for types. x_{3} will be a conjunction of du'u sumti, each possibly containing a bridi based on ctaipe. x_{4} need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent).

- cei'i
- pro-bridi: the universal predicate
- gai'o
- pro-bridi: the empty predicate
- mai'i
- pro-sumti: the universal argument/value; syntactically-contextually and type-permitted maximally generic in its typing
- zai'o
- pro-sumti: the empty argument/value; syntactically-contextually and type-permitted maximally generic in its typing