proposition: Lemma card_ran A B (e : {fhrel A & B}) : #|ran e| = #|ftop unit _⋅e|.
proof: Proof. rewrite (eq_card ran_dom) card_dom -card_cnv. apply: weq_card. rewrite /ftop_def. by rewrite cnvdot cnvtop cnv_invol. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)