Erm.v

Theorem identity_fn_applied_twice : 
  forall (f : bool -> bool),
    (forall (x : bool), f x = x) -> forall (b : bool), f (f b) = b.
Proof.
  intros f x b. (* Introduce our parameters *)
  destruct b as [| b']. (* destruct b for possible values of b' <-- I don't use this and it worries me *)
  rewrite -> x. (* rewrite f (f true) = true to f true = true *)
  rewrite -> x. (* rewrite f true = true to true = true *)
  reflexivity. (* solve the first subgoal above *)
  rewrite -> x. (* rewrite f (f false) = false to f false = false *)
  rewrite -> x. (* rewrite f false = false to false = false *)
  reflexivity. (* solve the second subgoal above *)
  Qed.  (* victory for zim *)
  
  
(* better version ! *)

Theorem identity_fn_applied_twice : 
  forall (f : bool -> bool),
    (forall (x : bool), f x = x) -> forall (b : bool), f (f b) = b.
Proof.
  intros f H b.
  rewrite -> H.
  rewrite -> H.
  reflexivity. Qed.

Theorem identity_fn_applied_twice : 
  forall (f : bool -> bool),
    (forall (x : bool), f x = x) -> forall (b : bool), f (f b) = b.
Proof.
  intros f H b. (* Introduce our parameters *)
  rewrite -> H.
  apply H.
Qed.

Thanks ! :D