simplified proofs for splitI and splitD, added splitD'
added split_conv_tac (also to claset()) as an optimization
made split_all_tac safe introducing safe_full_simp_tac,EXISTING PROOFS MAY FAIL
datatype ('a,'b)term = Var 'a | App 'b ((('a,'b)term)list)