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