Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many section variable.

For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.

0 files changed, 0 insertions, 0 deletions