let mk_inr = (Coproduct(In(Right)), 5)