proposition: Lemma Invariance3: forall x, invariant (reachable_covered x).
proof: Proof. unfold reachable_covered. intros; intros len g l r; simpl; intros. specialize (H0 y H1). destruct H0 as [z [? [? ?]]]. rewrite in_app_iff in H0. exists z; split; [| split]; auto. destruct_eq_dec g z; [| destruct H0; [tauto |]; destruct (in_dec equiv_dec z r); [| destruct H0; try tauto]]. + subst. rewrite in_app_iff; right. left; auto. + rewrite in_app_iff; right. right; auto. + rewrite in_app_iff. left. rewrite in_new_working_list. split. - rewrite in_app_iff. rewrite <- edge_func_step. unfold edge in H0; tauto. - pose proof valid_not_null G z. apply reachable_foot_valid in H3. simpl; tauto. Qed.
imports: Coq.Sets.Finite_sets Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Sorting.Permutation Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles Coq.Lists.List VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph