proposition: Lemma omega_exp_rw : forall a, nf a -> omega ^ a = phi0 a.
proof: Proof. unfold omega, phi0;simpl. intro a; elim a; simpl. trivial. destruct t. simpl. intros. generalize (nf_of_finite H1). intro; subst t. case n;simpl. auto. simpl. induction n0;simpl. auto. rewrite IHn0. simpl. auto. intros. unfold omega_term. rewrite H0. fold (phi0 t). fold (phi0 (cons (cons t1 n t2) n0 t)). fold (phi0 (cons (cons t1 n t2) n0 zero)). rewrite <- (plus_to_cons H1). rewrite phi0_plus_mult. unfold omega_term;auto. unfold omega_term;constructor. nf_inv. nf_inv. nf_inv. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List