The Coq mailing list

["窦亮" <ldou AT cs.ecnu.edu.cn>]

Hi guys, I have the following definition for a complicate inductive type s:

Definition name := string.

Definition lname := list string.

Definition pname := lname * lname.

 

Inductive s : Type :=

|basic_s : name -> pname -> s

|complex_s : name -> list s -> nat -> 

         list (name * s * set name * name * lname * set name * s * name) ->

         pname -> s

|complex_s2 : name -> set s -> pname -> s

.

Definition t := name * s * set name * name * lname * set name * s * name.

----------------------
you can see i rename a part of "complex_s" as t for better reference. 
My question is i don't know how to finish the proof for the decidable equality definition for t and s:
---------------------------

Definition s_dec : forall (a b : s) ,{a = b} + {a <> b}.
 

Definition t_dec : forall (a b : t) ,{a = b} + {a <> b}.