proposition: Lemma sound_fits_upath_transfer: forall p l (g1 g2: EdgeListGG), (forall v, vvalid g1 v <-> vvalid g2 v) -> (forall e, In e l -> evalid g2 e) -> fits_upath g1 l p -> fits_upath g2 l p.
proof: Proof. intros. apply (fits_upath_transfer'' p l g1 g2); intros. apply (valid_upath_vvalid g1 p) in H2. apply H; auto. apply valid_upath_exists_list_edges'. exists l; auto. apply H0; auto. repeat rewrite src_fst; auto. apply (fits_upath_evalid g1 p l); auto. repeat rewrite dst_snd; auto. apply (fits_upath_evalid g1 p l); auto. auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph