proposition: Lemma npe_sym: forall (m1 m2: NodePred Vertex), node_pred_equiv m1 m2 -> node_pred_equiv m2 m1.
proof: Proof. unfold node_pred_equiv; intros. specialize (H n); tauto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext