thus [x1,x2,x3] `3_3 = [[x1,x2],x3] `2
.= x3 ; :: thesis: verum