proposition: Lemma standard_path_unshift i alpha j beta : standard_path (S i) alpha (S j) beta -> standard_pathS i alpha j beta.
proof: Proof. intros; eapply standard_path_unshift_0; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)