reconsider s1 = NAT --> (0. S) as sequence of S ;
take s1 ; :: thesis: s1 is constant
thus s1 is constant ; :: thesis: verum