The function MAP2_CONV is a conversion for computing the result
of mapping a binary function f:ty1->ty2->ty3 down two lists
“[l11;...;l1n]” whose elements are of type ty1 and
“[l21;...;l2n]” whose elements are of type ty2. The lengths of
the two lists must be identical. The first
argument to MAP2_CONV is expected to be a conversion
that computes the result of applying the function f to a pair of
corresponding elements of these lists. When applied to a term
“f l1i l2i”, this conversion should return a theorem of the form
|- (f l1i l2i) = ri, where ri is the result of applying the function
f to the elements l1i and l2i.
Given an appropriate conv, the conversion MAP2_CONV conv takes a
term of the form “MAP2 f [l11;...;dl2tn] [l21;...;l2n]” and returns
where conv “f l1i l2i” returns |- (f l1i l2i) = ri for
i from 1 to n.
|- MAP2 f [l11;...;l1n] [l21;...;l2n] = [r1;...;rn]