(module c4_double_consume
  (data Pair
    (doc "boxed pair of ints")
    (ctor MkPair (con Int) (con Int)))
  (fn fst (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
    (body (match p (case (pat-ctor MkPair a b) a))))
  (fn snd (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
    (body (match p (case (pat-ctor MkPair a b) b))))
  (fn both
    (doc "MUST STAY RED: rest projected by fst AND snd = consumed twice")
    (type (fn-type (params (own (con Pair))) (ret (own (con Pair)))))
    (params rest)
    (body (term-ctor Pair MkPair (app fst rest) (app snd rest)))))