proposition: Lemma localDag_reachable_list_spec: forall g x S l, vvalid g x -> localDag g x -> step_list g x S -> reachable_list g x l -> reachable_set_list g S (remove equiv_dec x l).
proof: Proof. intros. intro y. specialize (H2 y). rewrite remove_In_iff. rewrite H2. rewrite (reachable_ind' g x S y H H1). assert (x = y <-> y = x) by (split; intros; congruence). assert (reachable_through_set g S y -> y <> x); [| tauto]. specialize (H0 x). spec H0; [apply reachable_refl; auto |]. intros [z [? ?]] ?. subst. specialize (H0 z). rewrite (H1 z) in H4. apply H0; auto. split; [| split]; auto. apply reachable_head_valid in H5; auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2