Open teorth opened 9 hours ago
Findings can be reported at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Outstanding.20equations.2C.20v1
The anti-implication to 1489 (which is stronger than 255) was settled by the translation-invariant method, see #675. However, this method does not suffice to resolve 255.
Findings can be reported at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Outstanding.20equations.2C.20v1