proposition: Lemma standard_gnaw_iota_from i alpha l : i <> 0 -> standard_gnaw i alpha l = gnaw alpha (iota_from i l).
proof: Proof. generalize i alpha; induction l. - reflexivity. - intros i0 alpha0 H;simpl; destruct i0. + now destruct H. + simpl; rewrite IHl; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)