proposition: Lemma mark_list_eq: forall root xs g1 g2, mark_list xs g1 g2 -> WeakMarkGraph.componded_mark_list root xs g1 g2 /\ g1 ~=~ g2.
proof: Proof. intros. change (mark_list xs g1 g2) with (relation_list (map (fun x => relation_conjunction (WeakMarkGraph.mark x) (respectful_relation pg_lg structurally_identical)) xs) g1 g2) in H. eapply relation_list_conjunction in H. rewrite relation_conjunction_iff in H. split. + destruct H as [? _]. eapply relation_list_inclusion; [| exact H]. intros ? _. clear. intros g1 g2 ?. exists g2; [| apply WeakMarkGraph.eq_do_nothing; auto]. exists g1; [apply WeakMarkGraph.eq_do_nothing; auto |]. auto. + eapply si_list. exact (proj2 H). Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.msl_application.Graph Coq.Logic.Classical