fact: Definition fhrel_dot (e1 : {fhrel A & B}) (e2 : {fhrel B & C}) : {fhrel A & C} := fun x y => [exists z, e1 x z && e2 z y].
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)