theorem appendeq2 (l1 _l21 _l22: nat): $ _l21 = _l22 -> l1 ++ _l21 = l1 ++ _l22 $;
_l21 = _l22 -> _l21 = _l22
_l21 = _l22 -> l1 ++ _l21 = l1 ++ _l22