Commit 2021-05-26 00:55 fd1c8e7f
View on Github →feat(data/list/forall2): add two lemmas about forall₂ and reverse (#7714) rel_reverse shows that forall₂ is preserved across reversed lists, forall₂_iff_reverse uses rel_reverse to show that it is preserved in both directions.