x1 is a value / proof of type / proposition x2 under context x3 in (type / logical) system x4.
Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: "x3 \vdash x", with x4 implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written "x3 \vdash x". x1 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. x1 can be filled by zi'o, which means that the proposition is unprovable. x2 can be filled by a set of which the x1 value is a member. It may be convenient to interpret lo'i as the gadri for types. x3 will be a conjunction of du'u sumti, each possibly containing a bridi based on ctaipe. x4 need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent).