proposition: Lemma triple_aux4_copy: forall (g g1 g2: Graph) (g1' g2': Graph') (M0: V -> Prop) es_done, let PV1 := reachable_by_through_set g (map (dst g) es_done) (Complement _ M0) in let PE1 := Intersection _ (weak_edge_prop PV1 g) (evalid g) in g ~=~ g1 -> forall son, extended_copy (Union _ M0 PV1) son (g1, g1') (g2, g2') -> forall e, Intersection E (weak_edge_prop (reachable_by g son (Complement _ (Union _ M0 PV1))) g) (evalid g) e -> ~ g |= son ~o~> dst g e satisfying (Complement _ (Union _ M0 PV1)) -> vvalid g (dst g2 e) -> vmap g2 (dst g2 e) = dst g2' (emap g2 e).
proof: Proof. intros. destruct H0 as [COPY_si [COPY_gprv [COPY_gpre [? [? COPY_bij]]]]]. apply H4. + pose proof weak_edge_prop_si (reachable_by g1 son (Complement _ (Union _ M0 PV1))) _ _ H. rewrite <- H in H5 at 1. rewrite Same_set_spec in H5. rewrite <- (H5 e); auto. + rewrite <- H in COPY_si. rewrite Intersection_spec in H1; destruct H1. erewrite si_dst1 in H2 by eauto. unfold Complement, Ensembles.In. rewrite Intersection_spec; split. - rewrite <- H. auto. - rewrite <- (proj1 H); auto. + rewrite <- H in COPY_si. destruct COPY_si as [_ [? _]]. rewrite Intersection_spec in H1. destruct H1 as [_ ?]. rewrite <- H5; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism