proposition: Lemma is_list_no_edge_loop: forall root s t, is_list root -> reachable g root s -> g |= s ~> t -> reachable g t s -> False.
proof: Proof. intros. destruct H1 as [? [? ?]]. rewrite step_spec in H4. destruct H4 as [e [? [? ?]]]. destruct H2 as [p ?]. assert (g |= (s, e :: nil) is s ~o~> t satisfying (fun _ => True)). { split; split; simpl; auto. + unfold strong_evalid. rewrite H5, H6. split; auto. + hnf. rewrite Forall_forall; intros; auto. } pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H7 H2). apply (is_list_no_loop root) in H8; auto. simpl. intro. inversion H9. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph