Starting a benchmark suite, with one bechmark based on the erfriemann
loop VC.
Added function for detecting and performing monotone substitutions in a
conclusion based on hypotheses.