--- presupposes equality.occ
--- presupposes nat.occ

( clist : Type -> Type )

---

( clist_nil : {T | Type} (clist T) )

( clist_cons : {T | Type} T -> (clist T) -> (clist T) )

---

( clist_append : {T | Type} (clist T) -> (clist T) -> (clist T) )

( clist_append_nil : !! {T : Type}{l : (clist T)}
  (EQ (clist_append (clist_nil | T) l) l) )

( clist_append_cons : !! {T : Type}{l : (clist T)}{h : T}{t : (clist T)}
  (EQ (clist_append (clist_cons h t) l) (clist_cons h (clist_append t l))) )

---

( clist_ind : {T : Type}{P : (clist T) -> Prop}
  (P (clist_nil | T)) ->
  ({h : T}{t : (clist T)} (P t) -> (P (clist_cons h t))) ->
  (All ? [l : (clist T)] (P l)) )

---

( clist_append_is_assoc : {T : Type}{l1,l2,l3 : (clist T)}
  (EQ (clist_append l1 (clist_append l2 l3)) (clist_append (clist_append l1 l2) l3)) )

---

( clist_single : {T | Type} T -> (clist T) )

( clist_single_ax : ?? {T : Type}{x : T}
  (EQ (clist_single x) (clist_cons x (clist_nil | T))) )

---

( clist_empty : {U | Type} (clist U) -> Prop )

( clist_empty_nil : ?? {U : Type} (clist_empty | U (clist_nil | U)) )

( clist_not_empty_cons : ?? {U : Type}{l : (clist U)}{u : U} 
  (Not (clist_empty | U (clist_cons u l))) )

( clist_not_empty_single : {U : Type}{l : (clist U)}{u : U} 
  (Not (clist_empty | U (clist_append l (clist_single u)))) )

---

( clist_in : {T | Type} (clist T) -> T -> Prop )

( clist_in_cons_0 : ?? {T : Type}{l : (clist T)}{x : T} 
  (clist_in (clist_cons x l) x) )

( clist_in_cons_1 : ?? {T : Type}{l : (clist T)}{x,y : T} 
  (clist_in l y) -> (clist_in (clist_cons x l) y) )

---

( clist_map : {U,V | Type} (U -> V) -> (clist U) ->(clist V) )

( clist_map_nil : !! {U,V : Type}{f : (U -> V)}
  (EQ (clist_map f (clist_nil | U)) (clist_nil | V)) )

( clist_map_cons : !! {U,V : Type}{f : (U -> V)}{x : U}{l : (clist U)}
  (EQ (clist_map f (clist_cons x l)) (clist_cons (f x) (clist_map f l))) )

--- 

( clist_select : {T | Type} (T -> Prop) -> (clist T) -> (clist T) )

( clist_select_nil : !! {T : Type}{P : (T -> Prop)}
  (EQ (clist_select P (clist_nil | T)) (clist_nil | T)) )

( clist_select_cons_1 : !! {T : Type}{P : (T -> Prop)}{x : T}{l : (clist T)}
  (P x) -> (EQ (clist_select P (clist_cons x l)) (clist_cons x (clist_select P l))) )

( clist_select_cons_2 : !! {T : Type}{P : (T -> Prop)}{x : T}{l : (clist T)}
  (Not (P x)) -> (EQ | Type | (clist T) (clist_select P (clist_cons x l)) (clist_select P l)) )

( done )