theorem elv (a: nat): $ a e. _V $;
x = a -> (T. <-> T.)
a e. {x | T.} <-> T.
a e. _V <-> T.
T.
a e. _V