-The fact that we traverse two terms semi-simultaneously is reflected
-by the nested generic function type that occurs as the result type of
-tfoldl. By "semi-simultaneously", we mean that we first fold over the
-first term and compute a LIST of generic functions to be folded over
-the second term. So the outermost generic function type is GenericQ
-because we compute a list of generic functions which is a kind of
-query. The inner generic function type is parameterised in a type
-constructor c so that we can instantiate twin traversal for
-transformations (T), queries (Q), and monadic transformations (M).
-The combinator tfoldl is also parameterised by a nested generic
-function which serves as the function to be mapped over the first term
-to get the functions to be mapped over the second term. The combinator
-tfoldl is further parameterised by gfoldl-like parameters k and z
-which however need to be lifted to k' and z' such that plain term
-traversal is combined with list traversal (of the list of generic
-functions). That is, the essence of multi-parameter term traversal is
-a single term traversal interleaved with a list fold. As the
-definition of k' and z' details, the list fold can be arranged by the
-ingredients of the term fold. To this end, we use a designated TWIN
-datatype constructor which pairs a given type constructor c with a
-list of generic functions.