FunExt: change argument order
HoTT: small improvements
Rename by-definition combinator for eq-reasoning
≡: Hide subst, expose tr...