proposition: Lemma ran_dom {A B} {e : {fhrel A & B}} : ran e =i dom e°.
proof: Proof. move => x. by rewrite !inE. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)