theorem thesn (a: nat): $ the (sn a) = a $;
a1 e. sn a <-> a1 = a
T. -> (a1 e. sn a <-> a1 = a)
T. -> the (sn a) = a
the (sn a) = a