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 !
Look at this file