proposition: Lemma remove_edge_valid_upath: forall (g: PGraph) e p l, valid_upath g p -> fits_upath g l p -> ~ In e l -> valid_upath (pregraph_remove_edge g e) p.
proof: Proof. intros. apply valid_upath_exists_list_edges'. apply (fits_upath_transfer' _ _ _ (pregraph_remove_edge g e)) in H0. exists l; apply H0. intros. simpl. split; auto. intros. simpl. unfold removeValidFunc. split. apply (fits_upath_evalid g p l); auto. unfold not; intros. subst e0. contradiction. 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