proposition: Lemma path_toS_zero alpha s : ~ path_toS alpha s zero.
proof: Proof. red; inversion 1. destruct H0; now apply H0. destruct H0; now apply H0. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)