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?

`distinct [a,b,c,d]`

?

It compiles down to exactly the disequalities

Ah, wonderful!

Last updated: Dec 07 2023 at 08:19 UTC