proposition: Lemma path_to_path_toS : forall alpha s beta, path_to beta s alpha -> path_toS beta (unshift s) alpha.
proof: Proof. induction 1. - destruct i as [| j]; [absurd (0 = 0); auto |]. left; auto. - destruct i as [| j]; [absurd (0 = 0); auto |]. right with gamma; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)