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