theorem takeeq2d (_G: wff) (l _n1 _n2: nat): $ _G -> _n1 = _n2 $ > $ _G -> take l _n1 = take l _n2 $;
_G -> l = l
_G -> _n1 = _n2
_G -> take l _n1 = take l _n2