proposition: Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT.
proof: Proof. move=> eq_pT; have [|g g1 g2 x] := @inj_card_bij (sig p) T _ val_inj. by rewrite eq_pT. rewrite -(g2 x); exact: valP. Qed.
imports: mathcomp(all_ssreflect)