update admitted coq proofs
some simplifications of for poke