let mk_inr =
  let sym = Coproduct(InR) in
    function
      | App(Coproduct(OutR), [x]) -> x
      | x -> mk_app sym [x]