theorem alleq2 (A: set) (_l1 _l2: nat): $ _l1 = _l2 -> (all A _l1 <-> all A _l2) $;
_l1 = _l2 -> _l1 = _l2
_l1 = _l2 -> (all A _l1 <-> all A _l2)