Commit 2025-09-11 15:40 e026378e
View on Github →feat(data): List.Chain' helper lemmas (#25812) Add two helpers lemmas to go from a List.Chain' hypothesis to a concrete predicate about two consecutive elements, one in the positive and one in the negative.