proposition: Lemma fhrel_univalent A B (e : {fhrel A & B}) : is_univalent e <-> forall x y y', e x y -> e x y' -> y = y'.
proof: Proof. split => [/@injective_cnv/fhrel_injective|H]. - rewrite /cnv/= => H ? ? ?; exact: H. - rewrite /is_univalent. cnv_switch. rewrite cnv1 cnvdot. rewrite -/(is_injective _) fhrel_injective => ? ? ?. exact: H. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)