proposition: Lemma construct_reachable_tail_preserve: forall lim p r, exists l', @construct_reachable _ _ _ _ G is_null _ (lim, p, r) = l' ++ r.
proof: Proof. intros lim p r. remember (lengthInput (lim, p, r)) as n. assert (lengthInput (lim, p, r) <= n) by intuition. clear Heqn. revert lim p r H. induction n; intros. + simpl in H. rewrite construct_reachable_unfold. destruct p. exists nil; rewrite app_nil_l; auto. destruct (le_dec lim (length r)). exists nil; rewrite app_nil_l; auto. exfalso; intuition. + simpl in H. rewrite construct_reachable_unfold. destruct p. exists nil; rewrite app_nil_l; auto. destruct (le_dec lim (length r)). exists nil; rewrite app_nil_l; auto. remember (@new_working_list _ _ is_null p (map (dst G) (edge_func G v)) (v :: r)). simpl. simpl in IHn. specialize (IHn lim l (v :: r)). assert (lim - length (v :: r) <= n) by (simpl; intuition). apply IHn in H0. destruct H0 as [l1 ?]. rewrite app_cons_assoc in H0. exists (l1 +:: v). 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