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(x,xx) => 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 ornament vzip from zip
    with forall 'a. forall 'b. forall +'length. 
      {to_list ['length] ['a]} ->
      {to_list ['length] ['b]} ->
      {to_list ['length] [('a,'b) pair]}

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(x,xx) => 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 ornament vzipm from zipm
    with forall 'a. forall 'b. forall +'l1. forall +'l2. forall +'lm.
      + [ ('l1,'l2,'lm) min ] ->  
      {to_list ['l1] ['a]} ->
      {to_list ['l2] ['b]} ->
      {to_list ['lm] [('a,'b) pair]}