sample datatype defs now use datatype_intrs, datatype_elims

ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works ZF/intr-elim/elim_rls: applied make_elim to succ_inject! ZF/fin: changed type_intrs in inductive def ZF/datatype/datatype_intrs, datatype_elims: renamed from data_typechecks, data_elims ZF/list: now uses datatype_intrs

tactic/fold_tac,fold_goals_tac: now handle critical pairs on the right sides of the defs