Require Import ssreflect ssrfun ssrbool eqtype.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma f_ipt_inv_id A (f : A -> A)
      (f_ipt : forall x, f (f x) = f x)
      (f_inv : involutive f) :
  forall x, f x = id x.
Proof. by move=> x; rewrite -f_ipt f_inv. Qed.