theorem alleq1 (_A1 _A2: set) (l: nat): $ _A1 == _A2 -> (all _A1 l <-> all _A2 l) $;
_A1 == _A2 -> _A1 == _A2
_A1 == _A2 -> (all _A1 l <-> all _A2 l)