proposition: Lemma finite_graph_join: forall (g: PreGraph V E) (PV1 PV2 PV: V -> Prop) (PE1 PE2 PE: E -> Prop), Prop_join PV1 PV2 PV -> Prop_join PE1 PE2 PE -> FiniteGraph (gpredicate_subgraph PV1 PE1 g) -> FiniteGraph (gpredicate_subgraph PV2 PE2 g) -> FiniteGraph (gpredicate_subgraph PV PE g).
proof: Proof. intros. constructor. + destruct X as [[l1 [?H ?H]] ?]. destruct X0 as [[l2 [?H ?H]] ?]. exists (l1 ++ l2). split. - apply NoDup_app_inv; auto. intros v ? ?. rewrite H2 in H5; rewrite H4 in H6. unfold Ensembles.In in H5, H6; simpl in H5, H6. rewrite Intersection_spec in H5, H6. destruct H5, H6, H as [_ ?]. apply (H v); auto. - intros v. rewrite in_app_iff. rewrite H2, H4. unfold Ensembles.In; simpl; rewrite !Intersection_spec. destruct H as [? _]; specialize (H v); tauto. + destruct X as [? [l1 [?H ?H]]]. destruct X0 as [? [l2 [?H ?H]]]. exists (l1 ++ l2). split. - apply NoDup_app_inv; auto. intros e ? ?. rewrite H2 in H5; rewrite H4 in H6. unfold Ensembles.In in H5, H6; simpl in H5, H6. rewrite Intersection_spec in H5, H6. destruct H5, H6, H0 as [_ ?]. apply (H0 e); auto. - intros e. rewrite in_app_iff. rewrite H2, H4. unfold Ensembles.In; simpl; rewrite !Intersection_spec. destruct H0 as [? _]; specialize (H0 e); tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas