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.
Equations
- One or more equations did not get rendered due to their size.