%sig Nat = {
  nat : type.
  z : nat.
  s : nat -> nat.
}.

%sig List = {
  % the "parameter"
  elt : type.

  list: type.
  nil : list.
  cons : elt -> list -> list.

  append : list -> list -> list -> type.
  appnil : append nil L L.
  appcons: append (cons E L) M (cons E N)
        <- append L M N.
%  %block e : block {x : elt}.
%  %worlds (e) (append L M N).
  %mode (append +L +M -N).
}.

%sig MAP = {
  a : type.
  b : type.
  f : a -> b -> type.

  %struct La : List = { elt := a. }.
  %struct Lb : List = { elt := b. }.
  map : La.list -> Lb.list -> type.
  map/nil : map La.nil Lb.nil.
  map/cons : map (La.cons H TL) (Lb.cons H' TL')
            <- f H H'
            <- map TL TL'.
}.

%struct N : Nat.
%struct L : List = { elt := N.nat. }.

inc : N.nat -> N.nat -> type.
inc/ : inc X (N.s X).

%struct M : MAP = {
  a := N.nat.
  b := N.nat.
  f := inc.
  %struct La := L.
  %struct Lb := L.
}.

%query 1 1 M.map (L.cons (N.s N.z) (L.cons N.z L.nil)) X.