proposition: Lemma predIT (T : eqType) (A B : pred T) : B =1 predT -> predI A B =i A.
proof: Proof. move => BT x. by rewrite !inE BT /= andbT. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)