Small Michelson proof, mainly to avoid losing it. Works on a function with casts without doing a simulation.