It now turns setoid equalities into Leibniz equalities when possible,
and substitutes those.