;  5            3
; f (x) = x /\ f (x) = x
;
; ==>
;
; f (x) = x


(=>
 (and 
  (= 
   (f (f (f (f (f x))))) 
   x)
  (= 
   (f (f (f x))) 
   x))
 (= (f x) x)
)