proposition: Lemma path_toS_gnawS : forall s alpha beta, path_toS beta s alpha -> beta = gnawS alpha s.
proof: Proof. induction 1; trivial. - simpl; now destruct H. - simpl; destruct H; now subst. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)