We define the property Distin, that all the elements of a list are distinct.
** Module lib_list_Distin Imports lib_list_Member lib_nat_Le $Distin : {s|Type}(list s)->Prop $Dis1 : {s|Type}Distin (nil s) $Dis2 : {s|Type}{a:s}{xs:list s}(not (Member a xs))->(Distin xs)-> Distin (cons a xs) $Distin_elim : {s|Type}{C_Distin:(list s)->Prop}(C_Distin (nil s))-> ({a:s}{xs:list s}(not (Member a xs))->(Distin xs)->(C_Distin xs)-> C_Distin (cons a xs))->{x1|list s}(Distin x1)->C_Distin x1 [[s|Type][C_Distin:(list s)->Prop][f_Dis1:C_Distin (nil s)] [f_Dis2:{a:s}{xs:list s}(not (Member a xs))->(Distin xs)-> (C_Distin xs)->C_Distin (cons a xs)][a:s][xs:list s] [x1:not (Member a xs)][x2:Distin xs] Distin_elim C_Distin f_Dis1 f_Dis2 (Dis1|s) ==> f_Dis1 || Distin_elim C_Distin f_Dis1 f_Dis2 (Dis2 a xs x1 x2) ==> f_Dis2 a xs x1 x2 (Distin_elim C_Distin f_Dis1 f_Dis2 x2)] Distin_inv = ... : {s|Type}{a|s}{l|list s}(Distin (cons a l))-> (not (Member a l) /\ Distin l) Distin_append = ... : {s|Type}{l1,l2:list s}(Distin l1)->(Distin l2)-> ({a:s}(Member a l1)->not (Member a l2))->Distin (append l1 l2) Distin_inj_map = ... : {s|Type}{u|Type}{l:list s}{f:s->u} ({a1,a2:s}(Member a1 l)->(Member a2 l)->(Eq (f a1) (f a2))-> Eq a1 a2)->(Distin l)->Distin (map f l) Distin_prod = ... : {s|Type}{u|Type}{l1:list s}{l2:list u}(Distin l1)->(Distin l2)-> Distin (prod_list l1 l2) Distin_inj_build = ... : {s|Type}{f:nat->s}{n:nat} ({k1,k2:nat}(Lt k1 n)->(Lt k2 n)->(Eq (f k1) (f k2))->Eq k1 k2)-> Distin (build_list f n) Distin_sublist_Le_length = ... : {s|Type}{xs,ys:list s}(Distin xs)-> ({a:s}(Member a xs)->Member a ys)->Le (length xs) (length ys)