# 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.

### Note

This result can be proved with a single call to `auto`.

Try to do it with basic tactics instead !
## Solution

Look at this file

Going home

Pierre Castéran