theorem nztailseq (_L1 _L2: nat): $ _L1 = _L2 -> nztails _L1 = nztails _L2 $;
_L1 = _L2 -> _L1 = _L2
_L1 = _L2 -> nztails _L1 = nztails _L2