add mk_is_in_thm which takes a ty and proves is_in for (mk_in ty)