proposition: Lemma wf_LT : forall alpha: T1, nf alpha -> Acc LT alpha.
proof: Proof. induction alpha as [| beta IHbeta n gamma IHgamma]. - split. intros y H0; inversion H0 as [_ [H3 _]]; destruct (not_lt_zero H3). - split; intros delta Hdelta. Abort. End First_attempt. Let Acc_strong (alpha:T1) := forall n beta, nf (cons alpha n beta) -> Acc LT (cons alpha n beta). Remark acc_impl {A} {R: A -> A -> Prop} (a b:A) : R a b -> Acc R b -> Acc R a. Proof. intros H H0; revert a H; now destruct H0. 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)