proposition: Lemma shiftLeft_app: forall v e x l1 l2, In (v, e) (shiftLeft x (l1 ++ l2)) <-> In (v, e) (shiftLeft x l1) \/ In (v, e) (shiftLeft (tailVertex x l1) l2).
proof: Proof. intros v e x. apply (rev_ind (fun l1 => forall l2, In (v, e) (shiftLeft x (l1 ++ l2)) <-> In (v, e) (shiftLeft x l1) \/ In (v, e) (shiftLeft (tailVertex x l1) l2))). - intros. simpl. intuition. - intros. rewrite <- app_assoc, <- app_comm_cons, app_nil_l. rewrite H. destruct x0 as [e' v']. simpl. rewrite H. simpl. rewrite tailVertex_foot. intuition. 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