ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually recursive datatypes, especially with monotone operators ZF/add_ind_def/add_fp_def: deleted as obsolete ZF/add_ind_def/add_fp_def_i: now takes dom_sum instead of domts. We no longer automatically construct a sum of separate domains, but could use a sum-closed set such as univ(A).