It now turns setoid equalities into Leibniz equalities when possible, and substitutes those.
Attach a file by drag & drop or click to upload
