proposition: Lemma const_pathS_eps_zero n alpha : const_pathS_eps n zero alpha -> alpha = zero.
proof: Proof. destruct 1; auto; now apply const_pathS_zero in H. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)