theorem mapeq2d (_G: wff) (F: set) (_l1 _l2: nat): $ _G -> _l1 = _l2 $ > $ _G -> map F _l1 = map F _l2 $;
_G -> F == F
_G -> _l1 = _l2
_G -> map F _l1 = map F _l2