proposition: Lemma omega_term_ambiguity : forall a n, nf a -> omega_term a n = (omega ^ a) * (F (S n)).
proof: Proof. intros a n H; rewrite omega_exp_rw. simpl. case a; simpl; unfold omega_term; auto. rewrite <- (plus_n_O n). auto. rewrite <- (plus_n_O n). auto. auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List