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