proposition: Lemma const_pathS_inv : forall n alpha beta, const_path (S n) alpha beta -> beta = canon alpha (S n) \/ const_path (S n) (canon alpha (S n)) beta.
proof: Proof. inversion 1; destruct H0. - left; congruence. - right; subst; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)