# Proving a logic riddle in Coq : testing equivalence in an Inductive set

I'm trying to formalize in Coq the following riddle and its solution

Alice, Bob and Charlie are one of each role:

• a truth teller (always tells the truth)
• a liar (always lies)
• and a spy (can lie or tell the truth)

They make the following statements:

• Alice: I am not a truth teller.
• Bob: I am not a spy.
• Charlie: I am not a liar.

What role is Charlie?
A. Truth teller
B. Liar
C. Spy
D. There is not enough information

I could progress alone , up to a point reached in the following file, because I cannot introduce the fact that two distinct roles are not equal to each other.

I tried a rewrite S in L as last step but I do not know which tactic to use next.I'm pretty sure there is something basic I'm missing.

Can anyone help?

The tactic discriminate(https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html?highlight=discriminate#coq:tacn.discriminate ) is made to handle the cases such as L: spy = liar
• In this case congruence also works, and you don't need to use the rewrite command beforehand.