proposition: Lemma pack_irrelevance (G : pre_graph) (graph_G graph_G' : is_graph G) : pack G graph_G ≃2 pack G graph_G'.
proof: Proof. iso2 bij_id bij_id xpred0; try exact: val_inj. split => // e [|]; exact: val_inj. Defined.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)