theorem appendeq1 (_l11 _l12 l2: nat): $ _l11 = _l12 -> _l11 ++ l2 = _l12 ++ l2 $;
_l11 = _l12 -> _l11 = _l12
_l11 = _l12 -> _l11 ++ l2 = _l12 ++ l2