proposition: Lemma mark1_componded_mark_list_mark: forall root l (g1 g2: Graph), vvalid g1 root -> (unmarked g1) root -> step_list g1 root l -> relation_list (nothing root :: mark1 root :: nothing root :: componded_mark_list root l :: nothing root :: nil) g1 g2 -> mark root g1 g2.
proof: Proof. intros root l g g2. intros. change (nothing root :: mark1 root :: nothing root :: componded_mark_list root l :: nothing root :: nil) with ((nothing root :: mark1 root :: nothing root :: componded_mark_list root l :: nil) +:: nothing root) in H2. erewrite app_same_relation in H2 by (rewrite @relation_list_tail; reflexivity). inversion H2; subst; rename y into g1. pose proof triple_mark1_componded_mark_list root l nil l g g1 H H0 H1 (eq_sym (app_nil_r _)) H3. cbv zeta in H5. apply (triple_nothing _ g1 g2 root l l nil H H0 H1 (eq_sym (app_nil_r _))) in H5. apply (triple_final root l g g2 H H0 H1 H5). auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Classes.Morphisms VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.lib.relation_list CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.subgraph2 CertiGraph.graph.dual_graph