Open teorth opened 5 hours ago
Findings can be reported at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Outstanding.20equations.2C.20v1
Informally claimed by Pace Nielsen, see above link.
Disclaimed by Pace Nielsen: the translation-invariant approach is insufficient to resolve the anti-implication.
Findings can be reported at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Outstanding.20equations.2C.20v1