theorem snoceq2d (_G: wff) (l _a1 _a2: nat): $ _G -> _a1 = _a2 $ > $ _G -> l |> _a1 = l |> _a2 $;
_G -> l = l
_G -> _a1 = _a2
_G -> l |> _a1 = l |> _a2