proposition: Lemma reachable_through_empty_eq (g: Gph): forall S, Same_set (reachable_through_set g S) (Empty_set V) <-> forall y, In y S -> ~ vvalid g y.
proof: Proof. intros; split. + induction S; intros; [unfold In; intros; tauto |]. intros. destruct (in_inv H0). - subst a; intro. destruct H. specialize (H y). spec H; [| inversion H]. unfold Ensembles.In. exists y. split; [apply in_eq | apply reachable_by_refl; [|hnf]; trivial]. - assert (Same_set (reachable_through_set g (a :: S)) (reachable_through_set g S)). 1: { split. + apply Extensionality_Ensembles in H; rewrite H. intro x; intro. inversion H2. + intro; intros. destruct H2 as [s [? ?]]. exists s; split; trivial; apply in_cons; trivial. } rewrite <- H2 in IHS. pose proof (IHS H y). apply H3; trivial. + intros. split; repeat intro. destruct H0 as [y [? ?]]. apply H in H0. apply reachable_head_valid in H1; tauto. hnf in H0; tauto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec