scheme 
List1=
class

type
List,Elem

value
empty :List,
cons:Elem><List->List,
head : List-~->Elem,
tail:List-~->List,
change_head:Elem><List-~->List

axiom
[head_cons] 
all e:Elem,l:List :- head(cons(e,l)) is e ,
[tail_cons] 
all e:Elem,l:List :- tail(cons(e,l)) is l ,
[change_head_cons]
all e,e1:Elem,l:List :- change_head(e1,cons(e,l)) is cons(e1,l) ,
[list_disjoint]
all e:Elem,l:List :- empty~=cons(e,l),
[list_induction]
all p:List ->Bool :-p(empty)/\(all e:Elem ,l:List :-p(l)=>p(cons(e,l)))=>(all l:List :-p(l))


end