proposition: Lemma path_toS_appR : forall u gamma alpha, path_toS gamma u alpha -> forall s t, s <> nil -> t <> nil -> u = s ++ t -> exists beta, path_toS beta s alpha /\ path_toS gamma t beta.
proof: Proof. induction 1. - intros. assert False. { destruct s, t; auto. simpl in H2. injection H2. intros. destruct s; try discriminate. } contradiction. - intros; destruct s. + destruct s0. * now destruct H1. * clear H1; simpl in H3; injection H3; intros; subst. symmetry in H1;apply app_eq_nil in H1. destruct H1; contradiction. + destruct s0. * now destruct H1. * simpl in H3; injection H3; intros. subst. destruct s0. -- simpl in *; exists gamma0; split. ++ left; auto. ++ subst t; auto. -- destruct (IHpath_toS (n1::s0) t); auto. ++ discriminate. ++ exists x; split; auto. ** now right with gamma0. ** destruct H5;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)