proposition: Lemma KS_thm_2_4_lemma3 : forall i n p alpha , nf alpha -> n < p -> const_pathS i (T1.cons alpha p zero) (T1.cons alpha n zero).
proof: Proof. induction 2. - apply KS_thm_2_4_lemma3_0; auto. - apply const_pathS_trans with (T1.cons alpha m zero); auto. + apply KS_thm_2_4_lemma3_0; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)