proposition: Lemma si_eq_as_set_reachable_through_set: forall (g1 g2: PreGraph V E) S1 S2 n, g1 ~=~ g2 -> eq_as_set S1 S2 -> (reachable_through_set g1 S1 n <-> reachable_through_set g2 S2 n).
proof: Proof. cut (forall (g1 g2 : PreGraph V E) S1 S2 (n : V), g1 ~=~ g2 -> eq_as_set S1 S2 -> (reachable_through_set g1 S1 n -> reachable_through_set g2 S2 n)). 1: intros; split; apply H; [| | symmetry | symmetry]; auto. intros. intros. unfold reachable_through_set in *. destruct H1 as [s [? ?]]. exists s; split. + pose proof proj1 H0 s. auto. + destruct (si_reachable g1 g2 s H). apply H3; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.find_not_in CertiGraph.graph.path_lemmas