Reduce proof obligations

[zamdzhiev]

When using the Unitary data type, it is sometimes required to satisfy proof obligations. This can make programming more difficult. Therefore, we should try to reduce this burden.

One idea is to use a monadic progamming discipline to introduce unitary operations as well. Essentially, we can try to have a very similar interface to QuantumOP, but without state preparation and without measurements, so that the operation we describe is indeed unitary.

This idea will be developed during an upcoming internship soon.

If someone happens to have some other idea or method in mind and is willing to share, then please let us know!