type 'a list
logic nil : 'a list
logic cons : 'a, 'a list -> 'a list
logic first : 'a list -> 'a
logic rest : 'a list -> 'a list
logic length : 'a list -> int

axiom L1: length(nil)=0
axiom L2: forall lst: 'a list. 
          not(lst=nil) -> length(lst)=1+length(rest(lst))

logic len: int
logic lst, temp: int list

goal intra_loop:
(not(temp=nil) and 
len=(length(lst)-length(temp))  ->
     (len+1)=(length(lst)-length(rest(temp))))


goal exit:
((temp=nil) and 
len=(length(lst)-length(temp))  ->
     len=length(lst))


goal start:
(true  ->
     0=(length(lst)-length(lst)))