proposition: Lemma succ_correct alpha beta : cnf beta = succ (cnf alpha) <-> Successor beta alpha.
proof: Proof. destruct alpha, beta; cbn; split. - intro; subst. split. + unfold ON_lt; red; cbn; red; red; repeat split; auto. apply lt_succ. + destruct z; unfold E0lt; cbn; intros. assert (cnf1 t1< cnf1)%t1. { repeat split; auto. apply lt_le_trans with (succ cnf0). destruct H0; auto with T1. now destruct H1. apply lt_succ_le; auto. apply H. } destruct H1. destruct H2. eapply T1.lt_irrefl; eauto. - destruct 1. unfold E0lt in H, H0. cbn in H, H0. destruct H. destruct H1. + apply lt_succ_le in H1; auto. * destruct H1; auto. specialize (H0 (E0_succ (mkord cnf_ok0))). cbn in H0; unfold LT in H0. exfalso. apply H0. -- split; auto with T1. split; auto with T1. ++ apply lt_succ;eauto with T1. ++ apply succ_nf; auto. -- split; auto with T1. apply succ_nf; auto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)