cbv_eval
This PR adds `cbv_eval` attribute that allows to evaluate functions in `cbv` tactic using pre-registered theorems.
Wojciech Różowski