theorem allal2 (A: set) (l: nat) {x: nat}: $ all A l <-> A. x (x IN l -> x e. A) $;
all A l <-> all A l
all A l <-> A. x (x IN l -> x e. A)