theorem zipeq2 (l1 _l21 _l22: nat): $ _l21 = _l22 -> zip l1 _l21 = zip l1 _l22 $;
_l21 = _l22 -> _l21 = _l22
_l21 = _l22 -> zip l1 _l21 = zip l1 _l22