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