proposition: Lemma gremove_predicate_partial_si: forall (g1 g2: Graph) (e: E) (root: V) (P: V -> Prop), out_edges g1 root e -> vvalid g1 root -> P root -> gremove_edge g1 e g2 -> (predicate_partialgraph g1 (fun n : V => ~ g1 |= root ~o~> n satisfying P)) ~=~ (predicate_partialgraph g2 (fun n : V => ~ g1 |= root ~o~> n satisfying P)).
proof: Proof. intros. destruct H2 as [? [? [? [? ?]]]]. assert (g1 |= root ~o~> src g1 e satisfying P). { destruct H. rewrite H7. apply reachable_by_refl; auto. } hnf. simpl. unfold predicate_vvalid. unfold predicate_weak_evalid. split; [|split; [|split]]; intros. - specialize (H2 v). intuition. - destruct_eq_dec e0 e. * subst. split; intro. destruct H8; exfalso; auto. destruct H6. destruct H8. exfalso; auto. destruct H6 as [? [? ?]]. rewrite H9. destruct H. destruct H8. intuition. * specialize (H3 _ H8). specialize (H4 _ H8). rewrite H3. split; intros; destruct H9; split; auto; assert (evalid g1 e0) by intuition; specialize (H4 H11 H9). rewrite <- H4; auto. rewrite H4. intuition. - intros. destruct H8. destruct H9. apply H4; auto. intro. subst. auto. - intros. destruct H8. destruct H9. apply H5; auto. intro. subst. auto. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical