proposition: Lemma Acc_strong_stronger : forall alpha, nf alpha -> Acc_strong alpha -> Acc LT alpha.
proof: Proof. intros alpha H H0; apply acc_impl with (phi0 alpha). - repeat split; trivial. + now apply lt_a_phi0_a. - apply H0; now apply single_nf. 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)