proposition: Lemma standard_gnaw_nf l : forall i alpha, nf alpha -> nf (standard_gnaw i alpha l).
proof: Proof. induction l. - cbn; auto. - intros; cbn ; destruct (T1_eq_dec (canon alpha i) zero) as [e|ne]. + rewrite e, standard_gnaw_zero; auto with T1. + apply IHl; destruct i. * cbn; auto with T1. apply nf_canon; eauto with T1. * now apply nf_canon. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)