proposition: Lemma reachable_by_through_app_strong': forall (g: PreGraph V E) P l1 l2, Same_set (Union _ (reachable_by_through_set g l1 P) (Complement _ (reachable_by_through_set g l1 P))) (Full_set _) -> Same_set (reachable_by_through_set g (l1 ++ l2) P) (Union _ (reachable_by_through_set g l1 P) (reachable_by_through_set g l2 (Intersection _ P (Complement _ (reachable_by_through_set g l1 P))))).
proof: Proof. intros. rewrite Same_set_spec. intros n. rewrite Union_spec. rewrite (reachable_by_through_set_eq_partialgraph_reachable_through_set _ _ l2), Intersection_comm, <- partial_partialgraph, <- reachable_by_through_set_eq_partialgraph_reachable_through_set. apply reachable_by_through_app_strong. clear n; intro n. rewrite Same_set_spec in H; specialize (H n). rewrite Union_spec in H. pose proof Full_set_spec _ n. unfold Complement, Ensembles.In in H. tauto. Qed.
imports: Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Classes.Morphisms Coq.Classes.Equivalence CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation