len (n |-> 0) = n ;
hence ex b₁ being empty-yielding NAT -valued FinSequence st b₁ is n -element ; :: thesis: verum