proposition: Lemma standard_path_unshift_0 i alpha j beta : standard_path i alpha j beta -> forall k l, i = S k -> j = S l -> standard_pathS k alpha l beta.
proof: Proof. induction 1. - intros k l H3 H4; subst; left; auto. injection H4; congruence. - intros; subst; right. apply IHstandard_path_to; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)