Guest User

Untitled

a guest
Nov 16th, 2015
278
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Require Import ssreflect ssrfun ssrbool eqtype.
  2.  
  3. Set Implicit Arguments.
  4. Unset Strict Implicit.
  5. Unset Printing Implicit Defensive.
  6.  
  7. Lemma f_ipt_inv_id A (f : A -> A)
  8.       (f_ipt : forall x, f (f x) = f x)
  9.       (f_inv : involutive f) :
  10.   forall x, f x = id x.
  11. Proof. by move=> x; rewrite -f_ipt f_inv. Qed.
RAW Paste Data