proposition: Lemma reachable_trans: forall x y z, reachable x y -> reachable y z -> reachable x z.
proof: Proof. intros. induction H0. + auto. + apply reachable_cons 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