proposition: Lemma log_nf : forall a, nf a -> nf (log a).
proof: Proof. destruct a;unfold log;simpl. constructor; eauto with T1. eauto with T1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List