proposition: Lemma boolPT (H : is_true p) : match boolP p with | AltTrue HT => T HT | AltFalse HF => F HF end = T H.
proof: Proof. destruct boolP. - congr T. rewrite (Eqdep_dec.eq_proofs_unicity _ i H) //. by move=> x y; have:= Bool.bool_dec x y => -[]; [left | right]. - by elim: (negP i). Qed.
imports: mathcomp(all_ssreflect fingroup perm)