proposition: Remark R4_3_2 : const_pathS_eps n2 beta (canon beta (S n1)).
proof: Proof. destruct (T1_eq_dec beta zero). - subst; cbn; now right. - left; apply Cor12_1 with n1; auto. + apply canonS_LT; auto. + left. split; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)