proposition: Corollary Cor12_3 (alpha : T1) : nf alpha -> forall beta i n, beta t1< alpha -> i <= n -> const_path i alpha beta -> const_path n alpha beta.
proof: Proof. destruct i, n. - auto. - inversion 3. - inversion 2. - intros; eapply Cor12_1 with i;eauto with arith. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)