simplifier
use patterns
Quantifier closing
