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

( list : Type -> Type )

---

( list_nil : {T | Type} (list T) )

( list_single : {T | Type} T -> (list T) )

( list_append : {T | Type} (list T) -> (list T) -> (list T) )

---

( list_append_assoc : || {T : Type}{l1,l2,l3 : (list T)}
  ((list_append l1 (list_append l2 l3)) = (list_append (list_append l1 l2) l3)) )

( list_append_right_id : || {T : Type}{l : (list T)} 
  ((list_append l (list_nil | T)) = l) )

( list_append_left_id : || {T : Type}{l : (list T)} 
  ((list_append (list_nil | T) l) = l) )

---

( list_empty : {U | Type} (list U) -> Prop )

( list_empty_nil : ?? {U : Type} (list_empty (list_nil | U)) )

( list_not_empty_single : ?? {U : Type}{l : (list U)}{u : U} 
  (Not (list_empty (list_append l (list_single u)))) )

---

( list_in : {T | Type} (list T) -> T -> Prop )

( list_in_single : ?? {T : Type}{l : (list T)}{x : T} 
  (list_in (list_append l (list_single x)) x) )

( list_in_append_l : ?? {T : Type}{l,l' : (list T)}{x : T} 
  (Not (list_empty l)) -> (Not (list_empty l')) -> (list_in l x) -> 
  (list_in (list_append l l') x) )

( list_in_append_r : ?? {T : Type}{l,l' : (list T)}{x : T} 
  (Not (list_empty l)) -> (Not (list_empty l')) -> (list_in l' x) -> 
  (list_in (list_append l l') x) )

( list_not_in_nil : ?? {T : Type}{x : T} 
  (Not (list_in (list_nil | T) x)) )

( list_not_in_single : ?? {T : Type}{x,y : T} 
  (Not (x = y)) -> (Not (list_in (list_single y) x)) )

( list_not_in_append : ?? {T : Type}{l,l' : (list T)}{x : T} 
  (Not (list_empty l)) -> (Not (list_empty l')) -> (Not (list_in l x)) -> (Not (list_in l' x)) -> 
  (Not (list_in (list_append l l') x)) )

---

( list_eq : {T | Type} (list T) -> (list T) -> Prop )

( list_eq_nil : ?? {T : Type}{l : (list T)} 
  (list_eq (list_nil | T) (list_nil | T)) )

( list_eq_append : ?? {T : Type}{l,l' : (list T)}{x : T} 
  (list_eq l l') -> (list_eq (list_append (list_single x) l) (list_append (list_single x) l')) )

( list_eq_refl : ?? {T : Type}{l : (list T)} 
  (list_eq l l) )

( list_eq_sym : {T : Type}{l,l' : (list T)} 
  (list_eq l l') -> (list_eq l' l) -> (list_eq l l') )

( list_eq_trans : {T : Type}{l,l',l'' : (list T)} 
  (list_eq l l') -> (list_eq l' l'') -> (list_eq l l'') )

( list_not_eq_1 : ?? {U : Type}{u : U}{l : (list U)} 
  (Not (list_eq (list_append l (list_single u)) (list_nil | U))) )

( list_not_eq_2 : ?? {U : Type}{u : U}{l : (list U)} 
  (Not (list_eq (list_nil | U) (list_append l (list_single u)))) )

( list_not_eq_3 : ?? {U : Type}{u,v : U}{l1,l2 : (list U)} (Not (u = v)) -> 
  (Not (list_eq (list_append (list_single u) l1) (list_append (list_single v) l2))) )

( list_not_eq_4 : ?? {U : Type}{u : U}{l1,l2 : (list U)} (Not (list_eq l1 l2)) -> 
  (Not (list_eq (list_append (list_single u) l1) (list_append (list_single u) l2))) )

---

( list_eq_implies_EQ : ?? {T : Type}{l,l' : (list T)}
  (list_eq l l') -> (l = l') )

( list_not_eq_implies_not_EQ : ?? {T : Type}{l,l' : (list T)}
  (Not (list_eq l l')) -> (Not (l = l')) )

---

( list_le : {T | Type} (list T) -> (list T) -> Prop )

( list_le_nil : ?? {T : Type}{m : (list T)} 
  (list_le (list_nil | T) m) )

( list_le_union_0 : ?? {T : Type}{m,m' : (list T)}{x : T} 
  (list_le m m') -> (list_le (list_append (list_single x) m) (list_append (list_single x) m')) )

( list_le_union_1 : ?? {T : Type}{m : (list T)}{x : T} 
  (Not (list_in m x)) -> (list_le m (list_append (list_single x) m)) )

( list_le_refl : ?? {T : Type}{m : (list T)} 
  (list_le m m) )

( list_le_trans : {T : Type}{m,m',m'' : (list T)} 
  (list_le m m') -> (list_le m' m'') -> (list_le m m'') )

---

( list_length : {T | Type} (list T) -> nat )

( list_length_nil : !! {T : Type}{x : T} 
  ((list_length (list_nil | T)) = 0) )

( list_length_single : !! {T : Type}{x : T} 
  ((list_length (list_single x)) = 1) )

( list_length_append : !! {T : Type}{l,l' : (list T)}{n,n' : nat}
  ((list_length (list_append l l')) = (nat_plus (list_length l) (list_length l'))) )

---

( list_occ : {T | Type} (list T) -> T -> nat )

( list_occ_nil : !! {T : Type}{x : T} 
  ((list_occ (list_nil | T) x) = 0) ) 

( list_occ_single_0 : !! {T : Type}{x,y : T} 
  (x = y) -> ((list_occ (list_single y) x) = 1) ) 

( list_occ_single_1 : !! {T : Type}{x,y : T} 
  (Not (x = y)) -> ((list_occ (list_single y) x) = 0) ) 

( list_occ_append : !! {T : Type}{l,l' : (list T)}{x : T} 
  (Not (list_empty l)) -> (Not (list_empty l')) ->
  ((list_occ (list_append l l') x) = (nat_plus (list_occ l x) (list_occ l' x))) )

---

( list_add : {T | Type} (list T) -> T -> (list T) )

( list_add_single : !! {T : Type}{l : (list T)}{x : T}
  ((list_add l x) = (list_append l (list_single x))) )

( list_in_add_eq : {T : Type}{l : (list T)}{x : T} 
  (list_in (list_add l x) x) )

( list_in_add_neq : {T : Type}{l : (list T)}{x,y : T} (Not (x = y)) ->
  (list_in (list_add l x) y) -> (list_in l y) )

---

( list_single_inj : {T : Type}{x,y : T} 
  ((list_single x) = (list_single y)) -> (x = y) )

---

( list_eq_occ := [T | Type][l,l' : (list T)] {x : T}
  ((list_occ l x) = (list_occ l' x)) )

---

( list_in_append_l_strong : {T : Type}{l,l' : (list T)}{x : T} (list_in l x) -> 
  (list_in (list_append l l') x) )

( list_in_append_r_strong : {T : Type}{l,l' : (list T)}{x : T} (list_in l' x) -> 
  (list_in (list_append l l') x) )

( list_in_append_strong : {T : Type}{l,l' : (list T)}{x : T}
  (list_in (list_append l l') x) -> (Or (list_in l x) (list_in l' x)) )

( list_in_single_implies_eq : {T : Type}{x,y : T} 
  (list_in (list_single x) y) -> (x = y) )

---

( list_mult : {T | Type}{n : nat} (list T) -> (list T) )

( list_mult_0 : !! {T : Type}{l : (list T)}
  ((list_mult 0 l) = (list_nil | T)) )

( list_mult_1 : !! {T : Type}{n : nat}{l : (list T)}
  ((list_mult (suc n) l) = (list_append (list_mult n l) l)) )

( list_occ_mult : {T : Type}{n : nat}{l : (list T)}{x : T}
  ((list_occ (list_mult n l) x) = (nat_mult n (list_occ l x))) )

--- 

( list_map : {U,V | Type} (U -> V) -> (list U) ->(list V) )

( list_map_nil : !! {U,V : Type}{f : (U -> V)}
  ((list_map f (list_nil | U)) = (list_nil | V)) )

( list_map_single : !! {U,V : Type}{f : (U -> V)}{x : U}
  ((list_map f (list_single x)) = (list_single (f x))) )

( list_map_union : !! {U,V : Type}{m,m' : (list U)}{f : (U -> V)}
  (Not (list_empty m)) -> (Not (list_empty m')) ->
  ((list_map f (list_append m m')) = (list_append (list_map f m) (list_map f m'))) )

--- 

( list_select : {T | Type} (T -> Prop) -> (list T) -> (list T) )

( list_select_nil : !! {T : Type}{P : (T -> Prop)}
  ((list_select P (list_nil | T)) = (list_nil | T)) )

( list_select_single_1 : !! {T : Type}{P : (T -> Prop)}{x : T}
  (P x) -> ((list_select P (list_single x)) = (list_single x)) )

( list_select_single_2 : !! {T : Type}{P : (T -> Prop)}{x : T}
  (Not (P x)) -> ((list_select P (list_single x)) = (list_nil | T)) )

( list_select_union : !! {T : Type}{m,m' : (list T)}{P : (T -> Prop)}
  (Not (list_empty m)) -> (Not (list_empty m')) ->
  ((list_select P (list_append m m')) = (list_append (list_select P m) (list_select P m'))) )

( list_le_select : {T : Type}{m : (list T)}{P : T -> Prop} 
  (list_le (list_select P m) m) )

( list_in_select : {T : Type}{m : (list T)}{P : (T -> Prop)}{x : T} 
  (list_in (list_select P m) x) -> (P x) )

---

( list_remove : {T | Type} (list T) -> T -> (list T) )

( list_remove_nil : !! {T : Type}{x : T}
  ((list_remove (list_nil | T) x) = (list_nil | T)) )

( list_remove_single_1 : !! {T : Type}{x,y : T}
  (Not (x = y)) -> ((list_remove (list_single x) y) = (list_single x)) )

( list_remove_single_2 : !! {T : Type}{x,y : T}
  (x = y) -> ((list_remove (list_single x) y) = (list_nil | T)) )

( list_remove_append : !! {T : Type}{l,l' : (list T)}{x : T}
  (Not (list_empty l)) -> (Not (list_empty l')) ->
  ((list_remove (list_append l l') x) = (list_append (list_remove l x) (list_remove l' x))) )

( list_in_remove : {T : Type}{l : (list T)}{x,y : T} 
  (list_in (list_remove l y) x) -> (Not (x = y)) )

( done )