Typechecking of inlined code

[dstebila]

• [ ] When the inliner tries to inline something, it should check that the type of the thing being inlined satisfies any type constraints.
• [ ] In the proof engine, once inlining has happened, the type checker should be run.
  • This might be related to how I want to use the UniformlyRandom type in game hops to ensure e.g. arguments to a PRF/KDF are uniformly random when applying the hop.