proposition: Lemma Canon_plus_inv n alpha beta : Canon_plus (S n) alpha beta -> beta = Canon alpha (S n) \/ Canon_plus (S n) (Canon alpha (S n)) beta.
proof: Proof. unfold Canon_plus, Canon; intro H; destruct (const_pathS_inv H). - left; apply E0_eq_intro, H0. - right; apply H0. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)