proposition: Corollary strong_evalid_dec: forall g {fg: FiniteGraph g} e, {strong_evalid g e} + {~ strong_evalid g e}.
proof: Proof. intros. destruct (evalid_dec g e). destruct (vvalid_dec g (src g e)). destruct (vvalid_dec g (dst g e)). left. split. auto. split; auto. all: right; unfold not; intros Htmp; destruct Htmp as [? [? ?]]; contradiction. 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