Using the relation Adjoin we define the membership relation between elements of some type and lists over that type.
** Module lib_list_Member Imports lib_list_Adjoin lib_list_prod Member = ... : {s|Type}s->(list s)->Prop not_Member_nil = ... : {s|Type}{a|s}not (Member a (nil s)) Mem_ind = ... : {s|Type}{l|list s}{a,b|s} iff (Member b (cons a l)) (Member b l \/ Eq a b) Member_Adjoin = ... : {s|Type}{l,al|list s}{a,b|s}(not (Eq a b))->(Adjoin a l al)-> (Member b al)->Member b l Member_map = ... : {s|Type}{u|Type}{l:list s}{a:s}{f:s->u}(Member a l)-> Member (f a) (map f l) Member_map_inv = ... : {s|Type}{u|Type}{l:list s}{b:u}{f:s->u}(Member b (map f l))-> Ex ([a:s](Member a l /\ Eq (f a) b)) Member_append = ... : {s|Type}{l1,l2:list s}{a:s} iff (Member a (append l1 l2)) (Member a l1 \/ Member a l2) Member_prod = ... : {s|Type}{u|Type}{l1:list s}{l2:list u}{p:prod s u} iff (Member p (prod_list l1 l2)) (Member (Fst p) l1 /\ Member (Snd p) l2) Member_build = ... : {s|Type}{f:nat->s}{n:nat}{a:s} iff (Member a (build_list f n)) (Ex ([k:nat](Lt k n /\ Eq (f k) a)))