proposition: Lemma guarded_bij_vmap_image_dec: forall (PV: V -> Prop) (PE: E -> Prop) vmap emap (G: PreGraph V E) (G': PreGraph V' E'), guarded_bij PV PE vmap emap G G' -> exists f: forall v, Decidable (image_set PV vmap v), True.
proof: Proof. intros. pose proof vmap_inj H. destruct H0 as [f ?]. assert (forall v, Decidable (image_set PV vmap v)). 1: { intros. specialize (H0 v). destruct (f v) eqn:?H; [left | right]; rewrite image_set_spec. + exists v0. destruct H0; split; auto. specialize (H2 _ H0). symmetry; apply H2; auto. + intros [v0 [? ?]]. apply (H0 v0 H2). symmetry; auto. } exists X; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation