```type ('a) list = Nil
| Cons of 'a * 'a list

type zero = Zero

type ('a) succ = Su

type ('length,'a) vec = INil with 'length = zero
| forall 'length2. ICons of 'a * ('length2,'a) vec
with 'length = 'length2 succ

let rec to_list : forall 'length. forall 'a. ('length,'a) vec -> 'a list =
fun ['length 'a] (v : ('length,'a) vec) =>
match v with
| INil => Nil['a]
| ICons['pred](x,xs) => Cons['a](x,to_list ['pred] ['a] xs)
end

let forall 'length 'a ornament to_list ['length] ['a] : ('length,'a) vec
-> 'a list

type ('a,'b) pair = Pair of 'a * 'b

let rec fail : forall 'a. 'a = fail

let rec zip : forall 'a. forall 'b. 'a list -> 'b list -> ('a,'b) pair list =
fun ['a 'b] (xs : 'a list) (ys : 'b list) =>
match xs with
| Nil =>
match ys with
| Nil => Nil[('a,'b) pair]
| Cons(_,_) => fail [('a,'b) pair list]
end
| Cons(x,xs') =>
match ys with
| Nil => fail [('a,'b) pair list]
| Cons(y,ys') => Cons[('a,'b) pair](Pair['a,'b](x,y),zip
['a] ['b] xs' ys')
end
end

let rec vzip : forall 'a. forall 'b. forall 'length. ('length,'a) vec
-> ('length,'b) vec -> ('length,('a,'b) pair) vec =
fun ['a 'b 'length] (xs0 : ('length,'a) vec) (ys : ('length,'b)
vec) =>
match xs0 with
| INil =>
match ys with
| INil => INil['length,('a,'b) pair]
| ICons['pred](_,_) => fail [('length,('a,'b) pair) vec]
end
| ICons['pred](x0,xs1) =>
match ys with
| INil => fail [('length,('a,'b) pair) vec]
| ICons['pred](x1,xs2) => ICons['length,('a,'b) pair,
???](Pair['a,'b](x0,x1),vzip ['a] ['b] [???]
xs1 xs2)
end
end

let rec zipm : forall 'a. forall 'b. 'a list -> 'b list -> ('a,'b) pair
list =
fun ['a 'b] (xs : 'a list) (ys : 'b list) =>
match xs with
| Nil =>
match ys with
| Nil => Nil[('a,'b) pair]
| Cons(_,_) => Nil[('a,'b) pair]
end
| Cons(x,xs') =>
match ys with
| Nil => Nil[('a,'b) pair]
| Cons(y,ys') => Cons[('a,'b) pair](Pair['a,'b](x,y),zipm
['a] ['b] xs' ys')
end
end

type ('a,'b,'c) min = forall 'a2 'b2 'c2. MinS of ('a2,'b2,'c2) min
with 'a = 'a2 succ * 'b = 'b2 succ * 'c = 'c2 succ
| MinZl with 'a = zero * 'c = zero
| MinZr with 'b = zero * 'c = zero

let rec vzipm : forall 'a. forall 'b. forall 'l1. forall 'l2. forall 'lm.
('l1,'l2,'lm) min -> ('l1,'a) vec -> ('l2,'b) vec -> ('lm,('a,'b)
pair) vec =
fun ['a 'b 'l1 'l2 'lm] (x0 : ('l1,'l2,'lm) min) (xs0 : ('l1,'a)
vec) (ys : ('l2,'b) vec) =>
match xs0 with
| INil =>
match ys with
| INil => INil['lm,('a,'b) pair]
| ICons['pred](_,_) => INil['lm,('a,'b) pair]
end
| ICons['pred](x1,xs1) =>
match ys with
| INil => INil['lm,('a,'b) pair]
| ICons['pred](x2,xs2) => ICons['lm,('a,'b) pair,???]
(Pair['a,'b](x1,x2),vzipm ['a] ['b] [???]
[???] [???] ???? xs1 xs2)
end
end

```