proposition: Lemma constant_to_standard_path (alpha beta : T1) (i : nat): nf alpha -> const_pathS i alpha beta -> zero t1< alpha -> {j:nat | standard_path (S i) alpha j beta}.
proof: Proof. intros H H0 H1; destruct (T1_eq_dec beta zero). - subst; apply standard_path_to_zero; auto. intro; subst; eapply LT_irrefl; eauto. - destruct (constant_to_standard H H0) as [x e]. destruct x as [| x]. + simpl in e; subst. destruct (@LT_irrefl beta). apply const_pathS_LT with i. * auto. * auto. + exists ( x + S i)%nat; subst beta; apply standard_gnaw_to_path. * intro; subst; eapply LT_irrefl;eauto. * discriminate. * intro H2; apply standard_gnaw_S_zero in H2; contradiction. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)