proposition: Lemma remove_edge_unaffected: forall (g: PGraph) e p, valid_upath (pregraph_remove_edge g e) p -> valid_upath g p.
proof: Proof. intros. pose proof (valid_upath_exists_list_edges _ p H). destruct H0 as [l ?]. apply valid_upath_exists_list_edges'. apply (fits_upath_transfer' _ _ _ g) in H0. exists l; auto. intros. split; auto. intros. apply (fits_upath_evalid (pregraph_remove_edge g e) p l) in H1. simpl in H1. unfold removeValidFunc in H1. apply H1. auto. auto. auto. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph