proposition: Lemma KS_thm_2_4_lemma4 : forall i alpha, nf alpha -> const_pathS i (T1.phi0 (succ alpha)) (T1.phi0 alpha).
proof: Proof. destruct i. - intros; left; rewrite canonS_phi0_succ_eqn; auto. split; [discriminate | reflexivity]. - intros; right with (canon (T1.phi0 (T1.succ alpha)) (S (S i))). + rewrite canonS_phi0_succ_eqn; auto. split; [discriminate | reflexivity]. + rewrite canonS_phi0_succ_eqn; auto. apply KS_thm_2_4_lemma3; auto with arith. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)