proposition: Lemma step_list_step_reachable: forall root s d l, reachable G root s -> reachable G root d -> G |= s ~> d -> step_list G root l -> reachable_through_set G l d.
proof: Proof. intros. rewrite (reachable_ind' _ l) in H; auto. 2: apply reachable_head_valid in H0; auto. destruct H. + subst s. exists d. split. - hnf in H2. rewrite H2. destruct H1 as [? [? ?]]. auto. - apply reachable_by_refl; auto. apply reachable_foot_valid in H0. auto. + apply reachable_through_set_step with s; auto. - apply reachable_foot_valid in H0; auto. - destruct H1 as [? [? ?]]; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.find_not_in CertiGraph.graph.path_lemmas