Introducing equality and disjunction

Prove the following theorem :

Theorem abcd_c : forall (A:Set)(a b c d:A), a=c \/ b= c \/ c=c \/ d=c.

This result can be proved with a single call to auto.
Try to do it with basic tactics instead !

Solution