This module contains the implementation of the embedded constraint substitution pass in the fixpoint
pipeline, substituting hypotheses of the form h : x = true in other hypotheses.
Substitute embedded constraints. That is look for hypotheses of the form h : x = true and use
them to substitute occurrences of x within other hypotheses. Additionally this drops all
redundant top level hypotheses.