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