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