thus [x1,x2,x3,x4] `4_4 = [[x1,x2,x3],x4] `2
.= x4 ; :: thesis: verum