proposition: Lemma standard_path_shift i alpha j beta : standard_pathS i alpha j beta -> standard_path (S i) alpha (S j) beta.
proof: Proof. induction 1. - left; auto. - right; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)