proposition: Lemma reachable_list_bigraph_in: forall {l1 l2 x} l r, vvalid G x -> reachable_list G l l1 -> reachable_list G r l2 -> (forall y, step G x y <-> y = l \/ y = r) -> forall y, reachable G x y <-> x = y \/ In y l1 \/ In y l2.
proof: Proof. intros. specialize (H0 y). specialize (H1 y). split; intro. + apply reachable_ind in H3. destruct H3 as [? | [z [[? [? ?]] [? ?]]]]; auto. rewrite H2 in *. destruct H5. - subst. rewrite <- H0 in H7. auto. - subst. rewrite <- H1 in H7. auto. + destruct H3 as [? | [? | ?]]. - subst. apply reachable_by_refl; auto. - rewrite H0 in H3. apply edge_reachable_by with l. * auto. * split; auto. split. apply reachable_head_valid in H3; auto. rewrite H2; auto. * apply H3. - rewrite H1 in H3. apply edge_reachable_by with r. * hnf; auto. * split; auto. split. apply reachable_head_valid in H3; auto. rewrite H2; auto. * apply H3. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.find_not_in CertiGraph.graph.path_lemmas