feat: bv_decide?

[hargoniX]

Closes: #66

A few open problems remain:

• the generation of the simp syntax is not pretty
• it also doesn't necessarily generate correct simp syntax apparently
• It generates indented tactic seqs for some reason, make it not do that.