proposition: Lemma limit_plus_F_inv0 : forall alpha beta, limit_plus_F alpha 0 beta -> nf alpha -> alpha = beta.
proof: Proof. intros. generalize (limit_plus_F_plus H H0). simpl. rewrite plus_alpha_0. auto. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo