proposition: Lemma path_toS_path_to alpha s beta : path_toS beta s alpha <-> path_to beta (shift s) alpha.
proof: Proof. split. - induction 1. + left; auto. + right with gamma; auto. - revert alpha beta; induction s. + inversion 1. + simpl; inversion 1. * assert (s = nil). { destruct s; trivial. discriminate. } subst s; simpl in H; inversion H. left; auto. inversion H10. * right with gamma; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)