The Coq mailing list

[zaman <zaman.a25 AT gmail.com>]

Hi. Im having a problem with my Coq Proof and was hoping for some help and 
guidance. I have part of my definition below:
       
    Inductive Architecture : Set := 
    | Create_Architecture (Arch_Name: string)(MyComponents: list Component)
(MyConnections: list Connector)

    with

    ...

    with 

    Connector : Set :=
    | Create_Connector (Con_Name:string) (client: Component)(server:Component)

I wish to say that "A component term must be either a client or server of a 
connection; but not both." I have come up with the following as a 
representation 
of the above in the coq (based on my definition above):

    (forall con:Connector, forall c:Component, In con (MyConnections x) -> 
    (c = (client con) /\ c <> (server con)) \/ (c <> (client con) /\ c = 
(server 
con)))

However, Im not sure if that is correct (is it?), as when i get to the proof, 
I 
get stuck at the point 

    5 subgoals
    con : Connector
    c : Component
    H0 : Connection1 = con
    ______________________________________(1/5)
    c = HotelRes

The type of HoteRes is indeed Component (in this case, HotelRes is the client 
of 
the connection), however, since this is not in the set of assumptions, I cant 
use something like the exact or auto tactics.

How could I proceed with such a proof? Thanks in advance.