proposition: Theorem nf_Acc (alpha : T1): nf alpha -> Acc LT alpha.
proof: Proof. induction alpha. - intro; apply Acc_zero. - intros; eapply Acc_implies_Acc_strong;auto. apply IHalpha1; eauto. apply nf_inv1 in H; auto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)