proposition: Lemma reachable_ind_reachable: forall x y, reachable G x y <-> ind.reachable G x y.
proof: Proof. intros; split; intros. + destruct H as [[v p] [[? ?] ?]]. simpl in H. subst. revert x H1. induction p; intros. - destruct H1. simpl in *. apply ind.reachable_nil. auto. - pose proof (good_path_tail _ _ _ H1). unfold ptail in H. specialize (IHp _ H). rewrite pfoot_cons. apply ind.reachable_cons with (dst G a); auto. clear H. destruct H1 as [? _]. apply valid_path_edge with p; auto. + induction H. - apply reachable_refl; auto. - apply edge_reachable with y; 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