proposition: Lemma cnvtop: top° ≡ @top X.
proof: Proof. rewrite -(parxtop top°) -{2}(cnvI top). by rewrite -cnvpar partopx cnvI. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures pttdom)