proposition: Lemma fhrel_surjective A B (e : {fhrel A & B}) : is_surjective e <-> forall y, exists x, e x y.
proof: Proof. split => [H y|H y ?]. - case/exists_inP : (H y y (eqxx _)) => x. by exists x. - move/eqP<-. apply/exists_inP. case: (H y) => x exy. by exists x. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)