proposition: Lemma pred_of_succ : forall beta, nf beta -> pred (succ beta) = Some beta.
proof: Proof. induction beta. - reflexivity. - simpl; destruct beta1. + intros; replace beta2 with zero. reflexivity. { T1_inversion H. auto. } + intros; simpl; destruct n. * destruct beta2. { reflexivity. } { simpl; destruct (beta2_1). - f_equal. cbn. apply nf_inv2 in H. T1_inversion H. subst;auto. - simpl; simpl in *; destruct (pred (succ beta2_2)). f_equal. injection IHbeta2. intro;subst;auto. eapply nf_inv2;eauto. discriminate IHbeta2. eapply nf_inv2;eauto. } * rewrite IHbeta2; auto. apply nf_inv2 in H; 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)