some lemmas about hypset_ok and term_union
prove sym and addAssum derived rules

and a so-far unsuccessful attempt to prove proves_ACONV