proposition: Lemma fits_upath_transfer'': forall p l g1 g2, (forall v, In v p -> vvalid g2 v) -> (forall e, In e l -> evalid g2 e) -> (forall e, In e l -> src g1 e = src g2 e) -> (forall e, In e l -> dst g1 e = dst g2 e) -> fits_upath g1 l p -> fits_upath g2 l p.
proof: Proof. induction p; intros. destruct l. auto. apply H3. destruct l. destruct p. simpl. apply H; left; auto. simpl in H3. contradiction. destruct p. simpl in H3. contradiction. split. assert (In e (e::l)). left; auto. + split. split. apply H0. left; auto. split. rewrite <- H1; auto. apply H. apply (fits_upath_vertex_src_In g1 _ (e::l) e); auto. rewrite <- H2; auto. apply H. apply (fits_upath_vertex_dst_In g1 _ (e::l) e); auto. rewrite <- H1; auto. rewrite <- H2; auto. destruct H3. destruct H3. auto. + apply (IHp l g1 g2). intros. apply H. right; auto. intros. apply H0. right; auto. intros. apply H1. right; auto. intros. apply H2. right; auto. apply H3. 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