operators:

generateurs

empty  :  () =>  empty
add: (list, nat) => list

observateurs

size: (list) => nat
nth: (s) => nat



AXIOMS:
size(empty) =0
size( add(list, n)) = succ(size(list))

Terminal Case
nth(add(list,n), 0)= n

#instead of x-1 in second part we put succ(x in first part of equation)
nth(add(list, succ(x)), x)= nth(list, x)