We need to activate autolifting for this:

 #(mode autolift) #(mode unfold)

We define lists:

 type 'a list = | Nil | Cons of 'a * 'a list

And a map function:

 let rec map f x = match x with | Nil -> Nil | Cons(x,xs) -> Cons(f x, map f xs)

We want to use vectors of three elements:

 type 'a vec3 = Vec3 of 'a * 'a * 'a

They are a specialization of lists:

 type ornament 'a list3 : 'a list => 'a vec3 with | Nil => ~ | Cons(x, (y, z) : 'a list2) => Vec3(x, y, z) and 'a list2 : 'a list => 'a * 'a with | Nil => ~ | Cons(y, z : 'a list1) => (y, z) and 'a list1 : 'a list => 'a with | Nil => ~ | Cons(z, () : 'a list0) => z and 'a list0 : 'a list => () with | Nil => () | Cons(x, xs) => ~
 #(push_env) let map_tuple = lifting map : ('a -> 'b) -> 'a list3 -> 'b list3 #(pop_env)
 let rec map_tuple f x = match x with | Vec3(x, y, z) -> begin match map_auto1 f (y, z) with | (y, z) -> Vec3(f x, y, z) end and map_auto1 f x = match x with | (x, x1) -> (f x, map_auto2 f x1) and map_auto2 f x = match map_auto3 f () with | () -> f x and map_auto3 f x = match x with | () -> ()

We can request inlining for this definition:

 #(mode inline) let map_tuple = lifting map : ('a -> 'b) -> 'a list3 -> 'b list3
 let map_tuple f x = match x with | Vec3(x, y, z) -> Vec3(f x, f y, f z)