Distinctness

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
 ** Label (!Distin!) Distin
 ** Label (!Distin elim!) Distin_elim
 ** Label (!Distin Dis1!) Dis1
 ** Label (!Distin Dis2!) Dis2
[[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)