proposition: Lemma is_list_no_self_loop: forall root s, vvalid G root -> is_list root -> reachable G root s -> G |= s ~> s -> False.
proof: Proof. intros. destruct H2 as [? [? ?]]. rewrite step_spec in H4. destruct H4 as [e [? [? ?]]]. assert (G |= (s, e :: nil) is s ~o~> s satisfying (fun _ => True)). { split; split; simpl; auto. + unfold strong_evalid. rewrite H5, H6. split; auto. + hnf. rewrite Forall_forall; intros; auto. } destruct H0 as [pf [? ?]]. apply H8 in H1. clear H8. destruct H1 as [ps [[? ?] ?]]. destruct ps as [v ps]. assert (v = root) by (destruct H1 as [[? _] _]; simpl in H1; auto). subst v. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H1 H7). unfold path_glue, fst, snd in H10. apply H8 in H10. inversion H10. pose proof (f_equal (@length Edge) H12). rewrite app_length in H11. simpl in H11. intuition. Qed.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List