proposition: Lemma guarded_lge_spec: forall PV PE (G1 G2: LGraph), guarded_labeled_graph_equiv PV PE G1 G2 <-> (((forall v, PV v -> (vvalid G1 v <-> vvalid G2 v)) /\ (forall e, PE e -> (evalid G1 e <-> evalid G2 e)) /\ (forall e, PE e -> evalid G1 e -> evalid G2 e -> src G1 e = src G2 e) /\ (forall e, PE e -> evalid G1 e -> evalid G2 e -> dst G1 e = dst G2 e)) /\ (forall v, PV v -> vvalid G1 v -> vvalid G2 v -> vlabel G1 v = vlabel G2 v) /\ (forall e, PE e -> evalid G1 e -> evalid G2 e -> elabel G1 e = elabel G2 e)).
proof: Proof. split; intros; (destruct H as [[? [? [? ?]]] [? ?]]; split; [split; [| split; [| split]] | split]); intros. + specialize (H v); simpl in H. rewrite !Intersection_spec in H. tauto. + specialize (H0 e); simpl in H0. rewrite !Intersection_spec in H0. tauto. + apply H1; simpl; rewrite !Intersection_spec; auto. + apply H2; simpl; rewrite !Intersection_spec; auto. + apply H3; split; auto. + apply H4; split; auto. + simpl. rewrite !Intersection_spec. specialize (H v); tauto. + simpl. rewrite !Intersection_spec. specialize (H0 e); tauto. + apply H1; simpl in H5, H6; rewrite !Intersection_spec in H5, H6; tauto. + apply H2; simpl in H5, H6; rewrite !Intersection_spec in H5, H6; tauto. + apply H3; simpl in H5, H6; rewrite !Intersection_spec in H5, H6; tauto. + apply H4; simpl in H5, H6; rewrite !Intersection_spec in H5, H6; tauto. 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 CertiGraph.graph.graph_gen