interpretation "term construction (atomic)" 'SItem I = (TAtom I).
interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
interpretation "term construction (atomic)" 'SItem I = (TAtom I).
interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).