goalw thy [newref_def] "hp x = None --> hp (newref hp) = None"; by (fast_tac (claset() addIs [selectI2EX] addss (simpset())) 1); qed_spec_mp "newref_None";