proposition: Lemma reachable_ind: forall x y, reachable G x y -> x = y \/ exists z, edge G x z /\ x <> z /\ reachable G z y.
proof: Proof. intros. rewrite reachable_ind_reachable in H. induction H. + left; auto. + destruct_eq_dec x y. - subst y. apply IHreachable. - right. exists y. rewrite reachable_ind_reachable in *; 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