nat : type.
z : nat.
s : nat -> nat.

max : nat -> nat -> nat -> type.
mzz : max z z z.
mzs : max z (s N) (s N).
msz : max (s N) z (s N).
mss : max (s N1) (s N2) (s N)
      <- max N1 N2 N.