proposition: Lemma Lemma_4_4_1 : forall s n alpha beta (Ha : nf alpha) (Hb : nf beta), sorted_ge n s -> const_pathS_eps n alpha beta -> const_pathS_eps (simple_last n s) (gnawS alpha s) (gnawS beta s).
proof: Proof. induction s. - intros; now cbn. - intros; cbn; apply IHs. + apply nf_canon;eauto. + apply nf_canon;eauto. + eapply sorted_tail'; eauto. + destruct (T1_eq_dec alpha T1.zero). * subst; assert (beta = T1.zero). { destruct H0. - now apply const_pathS_zero in H0. - now symmetry. } subst; now right. * eapply Lemma_4_3 with (n0 :=a);auto. apply Cor12_2 with n; auto. inversion H0; auto with arith. all: eapply sorted_head; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)