proposition: Lemma iso_stagnates (G H : tgraph2) : G ≃2p H -> measure H = measure G.
proof: Proof. case. move=>[l _]. by rewrite /measure (card_bij (iso_v l)) (card_bij (iso_e l)). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) GraphTheory(setoid_bigop structures mgraph pttdom mgraph2) GraphTheory(rewriting reduction open_confluence transfer)