theorem dropeq2d (_G: wff) (l _n1 _n2: nat): $ _G -> _n1 = _n2 $ > $ _G -> drop l _n1 = drop l _n2 $;
_G -> l = l
_G -> _n1 = _n2
_G -> drop l _n1 = drop l _n2