proposition: Lemma si_stronger_partial_labeledgraph: forall (g1 g2: Graph) (p1 p2 p1' p2' p: V -> Prop), (forall v, p1' v <-> p1 v /\ p v) -> (forall v, p2' v <-> p2 v /\ p v) -> (predicate_partial_labeledgraph g1 p1) ~=~ (predicate_partial_labeledgraph g2 p2)%LabeledGraph -> (predicate_partial_labeledgraph g1 p1') ~=~ (predicate_partial_labeledgraph g2 p2')%LabeledGraph.
proof: Proof. intros. split; [| split]. + eapply si_stronger_partialgraph; eauto. destruct H1 as [? _]. auto. + simpl. intros ? [? ?] [? ?]. destruct H1 as [_ [? _]]. specialize (H1 v); simpl in H1. firstorder. + simpl. intros ? [? ?] [? ?]. destruct H1 as [_ [_ ?]]. specialize (H1 e); simpl in H1. firstorder. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Classes.Morphisms 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 Coq.Lists.List CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind