DEV Community

Discussion on: Daily Challenge #168 - [Code golf] f (f (f b)) = f b

Collapse
 
jose_a_alonso profile image
José A. Alonso

Another proof in Isabelle/HOL

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by (cases b; cases "f True"; cases "f False"; simp)