The example lemma for injective authentication (https://github.com/tamarin-prover/manual/blame/59525bd2c117da7acf21e58412ea209d7bc02522/src/007_property-specification.md#L783) uses upper case "A" and "B" as the two agents, but all the other authentication lemmas use the lower case "a" and "b". This becomes super confusing because the description specifically mentions that "a"/"b" are the agents, and "A"/"B" are the roles of those agents, which (as far as I understand) is not the intention.
I'm happy to make this change myself, I'd just like a vague confirmation that it wasn't the intention to be referring to the role in the lemma.
The example lemma for injective authentication (https://github.com/tamarin-prover/manual/blame/59525bd2c117da7acf21e58412ea209d7bc02522/src/007_property-specification.md#L783) uses upper case "A" and "B" as the two agents, but all the other authentication lemmas use the lower case "a" and "b". This becomes super confusing because the description specifically mentions that "a"/"b" are the agents, and "A"/"B" are the roles of those agents, which (as far as I understand) is not the intention.
I'm happy to make this change myself, I'd just like a vague confirmation that it wasn't the intention to be referring to the role in the lemma.