proposition: Lemma path_to_S_iota_from : forall l i alpha beta, path_toS beta (iota_from i (S l)) alpha -> standard_path_toS (l + i)%nat beta i alpha.
proof: Proof. induction l as [| l IHl]. - left. + inversion H. * now destruct H1. * inversion H4. + intros; inversion H; auto. * now destruct H1. * inversion H4; auto. + reflexivity. - right; replace (S l + i)%nat with (l + S i)%nat. + apply IHl; inversion H; subst. destruct H2; now subst. + abstract lia. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)