[Merged by Bors] - feat: more lemmas about List.dedup and other lattice operations

[Merged by Bors] - feat: more lemmas about List.dedup and other lattice operations #6001