proposition: Lemma const_pathS_first_step : forall i alpha beta, const_pathS i alpha beta -> {beta = canon alpha (S i) } + {const_pathS i (canon alpha (S i)) beta}.
proof: Proof. intros; destruct (T1_eq_dec beta (canon alpha (S i))). - now left. - right; generalize n; induction H. + destruct n;auto. tauto. + intros; destruct H; now subst y. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)