let
sym_mk_inr () =
Coproduct
.inr