Raise the precedence of transitivity.
Add equiv-is-set.
Add Pi-is-set and Pi-is-prop.
Add trans-ap.