1deltype sum
2delconst INL
3delconst INR
4delconst ISL
5delconst ISR
6delconst OUTL
7delconst OUTR
8skipthm INL_DEF
9skipthm INR_DEF
10skipthm sum_TY_DEF
11skipthm sum_ISO_DEF
12delproof sum_axiom
13delproof INL_11
14delproof INR_11
15delproof INR_neq_INL
16skipthm datatype_sum
17