proposition: Lemma is_tree_sub_is_tree: forall (g: Gph) root, vvalid g root -> is_tree g root -> forall v, step g root v -> is_tree g v.
proof: Proof. repeat intro. assert (reachable g root y) by (apply step_reachable with v; auto). specialize (H0 _ H3). destruct H0 as [proot [? ?]]. destruct H2 as [p ?]. exists p. split; auto. intro p'. intros. rewrite step_spec in H1. destruct H1 as [e [? [? ?]]]. assert (forall path, g |= path is v ~o~> y satisfying (fun _ : V => True) -> g |= (root, e :: nil) +++ path is root ~o~> y satisfying (fun _ : V => True)). { intro ppp; intros. clear -H H1 H6 H7 H8. apply reachable_by_path_merge with v; auto. split; split; simpl; auto. + split; auto. hnf. apply reachable_by_path_is_reachable in H8. apply reachable_by_head_valid in H8. subst. auto. + hnf. rewrite Forall_forall; intros; auto. } pose proof (H8 _ H2). pose proof (H8 _ H5). pose proof (H4 _ H9). pose proof (H4 _ H10). rewrite H11 in H12. inversion H12. destruct p as [v1 p1]. destruct p' as [v2 p2]. simpl in H14. f_equal; auto. clear -H2 H5. apply reachable_by_path_head in H2. simpl in H2. apply reachable_by_path_head in H5. simpl in H5. subst. auto. 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