proposition: Lemma reachable_ind2_reachable: forall x y, reachable G x y <-> ind2.reachable G x y.
proof: Proof. intros. rewrite reachable_ind_reachable. split; intros. + induction H. - apply ind2.reachable_nil; auto. - apply ind2.reachable_trans with y; auto. apply ind2.reachable_cons with x; auto. apply ind2.reachable_nil. destruct H; tauto. + induction H. - apply ind.reachable_nil; auto. - apply ind.reachable_trans1 with y; auto. apply ind.reachable_cons with z; auto. apply ind.reachable_nil. destruct H0; tauto. 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