proposition: Lemma Lemma_4_3 : forall alpha beta : T1, nf alpha -> nf beta -> forall n0 n1 n2 : nat, (n0 <= n2)%nat -> (n1 <= n2)%nat -> const_pathS_eps n0 alpha beta -> const_pathS_eps n2 (canon alpha (S n2)) (canon beta (S n1)).
proof: Proof. intros. destruct (T1_eq_dec alpha zero). - subst; destruct H3. + destruct (const_pathS_zero H3). + subst; cbn; now right. - eapply Lemma_4_3_0 with n0;eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)