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