6.5. Scope🔗

The tactic handles goals where all draws are independent uniform samples, the bodies are identical modulo variable permutation, and the only structural difference is draw order and unused draws.

It does not handle dependent draws, conditional branches, different body structures, or computational indistinguishability arguments.