proposition: Lemma succ_nf : forall alpha : T1 , nf alpha -> nf (succ alpha).
proof: Proof. induction alpha. - simpl;repeat constructor; auto with arith. - simpl; generalize IHalpha1 ; case alpha1. + simpl;repeat constructor; auto. + intros c n0 c0 H H0; apply nf_intro. * eapply nf_inv1; eauto. * apply IHalpha2; eapply nf_inv2 ; eauto. * apply succ_lt_a_phi0_b; eapply lt_a_phi0_b_intro; eauto. 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)