proposition: Lemma lcbe_rev_cons_inv: forall v root l, G |= root ~> v -> list_composed_by_edges (rev (root :: l)) -> list_composed_by_edges (rev (v :: root :: l)).
proof: Proof. intros. rewrite <- (app_nil_l (root :: l)), app_comm_cons, rev_app_distr. simpl rev at 2. unfold list_composed_by_edges in *. intros. destruct l2. + simpl in H1. rewrite <- (app_nil_l (d :: nil)), (app_comm_cons nil (d :: nil) s) in H1. rewrite app_assoc in H1. do 2 (apply app_inj_tail in H1; destruct H1). subst. auto. + assert (v0 :: l2 <> nil) by (intro; inversion H2). apply exists_last in H2. destruct H2 as [l' [a ?]]. rewrite e in H1. rewrite app_comm_cons, (app_comm_cons (d :: l') (a :: nil) s), app_assoc in H1. apply app_inj_tail in H1. destruct H1. apply (H0 l1 l'); auto. 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