daily pastebin goal
59%
SHARE
TWEET

Untitled

a guest Nov 16th, 2015 202 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
Top