proposition: Lemma Lemma_4_3_0 : const_pathS_eps n2 (canon alpha (S n2)) (canon beta (S n1)).
proof: Proof. destruct (LE_LT_eq_dec R4_3_4). - left. eapply Proposition_2_3a with (alpha := alpha); auto. generalize R4_3_3; inversion 1; auto. rewrite <- H2 in l; destruct (@LT_irrefl alpha). apply LT_trans with (canon alpha (S n2)); auto. apply canonS_LT;auto. now left. - rewrite e; now right. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)