Commit 2023-07-06 12:09 e1889c39

View on Github →

feat(Data/List/TFAE): version of forall_congr' for TFAE (#5624)

Estimated changes

added theorem List.exists_tfae
added theorem List.forall_tfae