proposition: Lemma univalent_card A B (e : {fhrel A & B}) : is_univalent e -> #|e| <= #|A|.
proof: Proof. move => ?. rewrite -card_cnv. exact: injective_card. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)