Dependent forall_congr

Stream: Is there code for X?

[Yaël Dillies]

Could we generalize docs#forall₂_congr and friends to dependent functions? It's very annoying they don't work on bounded quantifiers, as in ∀ a ∈ s, P a ↔ ∀ a ∈ s, Q a.

[Yaël Dillies]

Oh wait, the linkifier breaks because of the ₂. Anything we can do about that?

[Kevin Buzzard]

Right now the workaround is just to post the full URL https://leanprover-community.github.io/mathlib_docs/logic/basic.html#forall%E2%82%82_congr but I'd also be interested in hearing about a workaround (Eric also had a broken linkifier link yesterday for another reason IIRC)

[Kevin Buzzard]

Change the def to a dependent theorem and push to a branch to see how much breaks...

[Yury G. Kudryashov]

PR?