proposition: Lemma not_reachable_gen_dst_equiv: forall (g: Graph) x e y z, ~ reachable g x (src g e) -> reachable (pregraph_gen_dst g e y) x z <-> reachable g x z.
proof: Proof. intros. split; intro. - destruct H0 as [[p l] ?]. assert (~ In e l). { intro. apply (in_split_not_in_first EE) in H1. destruct H1 as [l1 [l2 [? ?]]]. subst l. apply reachable_by_path_app_cons in H0. destruct H0 as [? _]. rewrite no_edge_gen_dst_equiv in H0. 2: simpl; auto. simpl src in H0. apply H. exists (p, l1). auto. } rewrite no_edge_gen_dst_equiv in H0. 2: simpl; auto. exists (p, l). auto. - destruct H0 as [[p l] ?]. assert (~ In e l). { intro. apply in_split in H1. destruct H1 as [l1 [l2 ?]]. subst l. apply reachable_by_path_app_cons in H0. destruct H0 as [? _]. apply H. exists (p, l1). auto. } exists (p, l). rewrite no_edge_gen_dst_equiv; auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 Coq.Lists.List CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind