ctaipe fu'ivla

x1 is a value/proof of type/proposition x2 in (type/logical) system x3

A better definition; proposed by la .mudri.


In notes:

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