proposition: Lemma reachable_ind': forall x S y, vvalid G x -> step_list G x S -> (reachable G x y <-> x = y \/ reachable_through_set G S y).
proof: Proof. intros. unfold reachable_through_set. split; intros. + apply reachable_ind in H1. destruct H1; [left; auto | right]. destruct H1 as [z ?]; exists z. split; [| tauto]. rewrite (H0 z). destruct H1 as [[? [? ?]] ?]. auto. + destruct H1 as [? | [? [? ?]]]. - subst; apply reachable_refl; auto. - rewrite (H0 x0) in H1. apply edge_reachable with x0; auto. split; [| split]; auto. apply reachable_head_valid in H2; 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