proposition: Corollary Cor12_1 (alpha : T1) : nf alpha -> forall beta i n, beta t1< alpha -> i <= n -> const_path (S i) alpha beta -> const_path (S n) alpha beta.
proof: Proof. intros H beta i n H0 H1 H2; rewrite Nat.lt_eq_cases in H1; destruct H1. - eapply Cor12;eauto. - now subst. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)