daily pastebin goal
39%
SHARE
TWEET

Untitled

a guest Nov 16th, 2015 205 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
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top