proposition: Lemma fhrel_injective A B (e : {fhrel A & B}) : is_injective e <-> forall x x' y, e x y -> e x' y -> x = x'.
proof: Proof. rewrite /is_injective; split => [H x x' y E1 E2|H x x' E]. - apply/eqP. apply: (H x x'). by apply/exists_inP;exists y. - apply/eqP. case/exists_inP : E. exact: H. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)