proposition: Lemma lcbe_rev_cons: forall v l, list_composed_by_edges (rev (v :: l)) -> list_composed_by_edges (rev l).
proof: Proof. intros. rewrite <- (app_nil_l l), app_comm_cons, rev_app_distr in H. simpl in H. unfold list_composed_by_edges in *. intros. specialize (H l1 (l2 +:: v) s d). apply H. rewrite H0. rewrite <- app_assoc. simpl. 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