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