proposition: Lemma Lemma_4_4_0 : forall n p alpha beta (Halpha : alpha <> T1.zero), nf alpha -> nf beta -> (n <= p)%nat -> const_pathS_eps n alpha beta -> const_pathS_eps p (canon alpha (S p)) (canon beta (S p)).
proof: Proof. intros; inversion H2. - eapply Lemma_4_3_0 with n;auto. - right. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)