theorem ziplen (l1 l2: nat): $ len (zip l1 l2) = min (len l1) (len l2) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lenlfn | len (lfn (\ a1, nth a1 l1 - 1, nth a1 l2 - 1) (min (len l1) (len l2))) = min (len l1) (len l2) |
|
2 | 1 | conv zip | len (zip l1 l2) = min (len l1) (len l2) |