proposition: Lemma is_test_alt x: dom x ≡ x <-> x∥1 ≡ x.
proof: Proof. split=>E. - rewrite -{1}E -{1}(dotx1 (dom x)) -A14. by rewrite par11 dotx1. - by rewrite -E -{1}cnv1 -A10 dotx1 parC. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)