Collected notes

To discuss

• Move strs:StrSearch to the nextprefix just like we did for the literal? Then running the anchored engine would not require this? -> Yes!
• Project title

Action items

• Move strs:StrSearch to the optional of nextprefix in the PikeVM -> done
• If there is time, prove the “do prefix acc once” for the version of engines -> done
• Try to find a small reproduction of the issue with typeclass instances in proofs. Maybe this issue appears when we use #[refine]? -> done, issue was using Qed instead of Defined

Finish up last sections and resolve todos.