let x1, x2, x3, x4 be object ; :: thesis: len <%x1,x2,x3,x4%> = 4
thus len <%x1,x2,x3,x4%> = (len <%x1,x2,x3%>) + 1 by Th72
.= 3 + 1 by Th36
.= 4 ; :: thesis: verum