fact: Fixpoint nat_2_term (n:nat) : term := match n with 0 => (Term nat_0 nil) | S p => Term nat_S ((nat_2_term p)::nil) end.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List