theorem zipeq1 (_l11 _l12 l2: nat): $ _l11 = _l12 -> zip _l11 l2 = zip _l12 l2 $;
_l11 = _l12 -> _l11 = _l12
_l11 = _l12 -> zip _l11 l2 = zip _l12 l2