proposition: Lemma constant_to_standard (alpha beta : T1) (n : nat): nf alpha -> const_pathS n alpha beta -> {l : nat | standard_gnaw (S n) alpha l = beta}.
proof: Proof. intros H H0; destruct (T1_eq_dec beta zero). - subst beta; destruct (standard_gnaw_to_zero H (S n)). now exists x. - apply constant_to_standard_0;auto. apply not_zero_lt; auto. now apply const_pathS_nf with n alpha. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)