;  4            2
; f (x) = x /\ f (x) = x
;
; ==>
;
; f (x) = x


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