[#885] Replace FrameInstr with a function

Description

Problem: FramedInstr was intially introduced as a hack to avoid proving things to GHC. It does introduce some complications, however, and interpretation of FramedInstr is linear in the size of the input stack, which with nested frames can add up fast. Furthermore, optimizer doesn't handle FramedInstr properly.

Solution: Proper proofs turn out to be somewhat impractical, as that would force us to carry a lot of KnownList everywhere. But if we ignore Any and bottoms for a second, assume KnownList and stub proofs with unsafeCoerce at runtime (which is also very much desirable from the performance standpoint), turns out such proofs are ultimately pretty safe: most proofs have to be sound because inputs are traversed by type families deep enough as to not allow Any or a stuck type family break things. So unless we pass bottoms to theorems, things shouldn't break (and if we do, things will break in other places regardless)

This MR also does some minor chores that help with this and deprecates a few not-exactly-safe functions that became redundant. Additionally, it reuses the proof stubbing mechanism for Peano proofs and cleans up those proofs somewhat.

Related issue(s)

Resolves #885 (closed)

✅ Checklist for your Merge Request

Related changes (conditional)

• Tests (see short guidelines)

  • If I added new functionality, I added tests covering it.
  • If I fixed a bug, I added a regression test to prevent the bug from silently reappearing again.

• Documentation

  • I checked whether I should update the docs and did so if necessary:
    • Root README and other README.md files
    • Haddock
    • docs/
  • I updated changelog files of all affected packages released to Hackage if my changes are externally visible.

Stylistic guide (mandatory)

• My commits comply with the following policy.
• My code complies with the style guide.