fact: Definition dijkstra_correct (g : DijkGG) src popped prev dist : Prop := forall dst, vvalid g dst -> inv_popped g src popped prev dist dst /\ inv_unpopped g src popped prev dist dst /\ inv_unseen g src popped prev dist dst.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph