Jakub Kądziołka (Jan 26 2021 at 12:17): Jakub Kądziołka (Jan 26 2021 at 12:17):I need to express the assumption that a, b, c and d are pairwise unequal. I'm currently using card {a, b, c, d} = 4, but that's a very automation-hostile form - sledgehammer can barely prove a ~= b. Are there any better options?
Mathias Fleury (Jan 26 2021 at 12:19):distinct [a,b,c,d]?
Mathias Fleury (Jan 26 2021 at 12:20):It compiles down to exactly the disequalities
Jakub Kądziołka (Jan 26 2021 at 12:22):Ah, wonderful!
Last updated: Nov 13 2025 at 04:27 UTC