a guest Nov 16th, 2015 205 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
- 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.
RAW Paste Data