theorem elList (A: set) (l: nat): $ l e. List A <-> all A l $;
n = l -> (all A n <-> all A l)
l e. {n | all A n} <-> all A l
l e. List A <-> all A l