The basic file contains the definition of list and the usual elimination, reduction, iteration and double elimination rules plus the characterisation theorems.
** Module lib_list Imports lib_eq_basics $list : (Type)->Type(list) $nil : {t:Type}list t $cons1 : {t:Type}t->(list t)->list t $list_elim : {t:Type}{C_list:(list t)->Type}(C_list (nil t))-> ({x1:t}{x2:list t}(C_list x2)->C_list (cons1 t x1 x2))->{z:list t} C_list z [[t:Type][C_list:(list t)->Type][f_nil:C_list (nil t)] [f_cons1:{x1:t}{x2:list t}(C_list x2)->C_list (cons1 t x1 x2)][x1:t] [x2:list t] list_elim t C_list f_nil f_cons1 (nil t) ==> f_nil || list_elim t C_list f_nil f_cons1 (cons1 t x1 x2) ==> f_cons1 x1 x2 (list_elim t C_list f_nil f_cons1 x2)] cons = ... : {t|Type}t->(list t)->list t list_rec = ... : {s|Type}{t|Type}t->(s->(list s)->t->t)->(list s)->t list_iter = ... : {s|Type}{t|Type}t->(s->t->t)->(list s)->t list_ind = ... : {s|Type}{P:(list s)->Prop}(P (nil s))-> ({x:s}{l:list s}(P l)->P (cons x l))->{l:list s}P l list_double_elim = ... : {s|Type}{T:(list s)->(list s)->Type}(T (nil s) (nil s))-> ({x:s}{l:list s}(T (nil s) l)->T (nil s) (cons x l))-> ({x:s}{l:list s}({l':list s}T l l')->T (cons x l) (nil s))-> ({x:s}{l:list s}({l':list s}T l l')->{y:s}{l':list s} (T (cons x l) l')->T (cons x l) (cons y l'))->{l,l':list s}T l l' is_nil = ... : {t|Type}(list t)->Prop is_cons = ... : {t|Type}(list t)->Prop nil_or_cons = ... : {t|Type}{l:list t}(is_nil l \/ is_cons l) nil_not_cons = ... : {t|Type}{l:list t}{x:t}not (Eq (nil t) (cons x l))