fact: Definition structurally_identical (g1 g2: PreGraph Vertex Edge): Prop := (forall v : Vertex, (vvalid g1 v <-> vvalid g2 v)) /\ (forall e : Edge, (evalid g1 e <-> evalid g2 e)) /\ (forall e : Edge, evalid g1 e -> evalid g2 e -> src g1 e = src g2 e) /\ (forall e : Edge, evalid g1 e -> evalid g2 e -> dst g1 e = dst g2 e).
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext