fact: Fixpoint omega_tower (n:nat) : T1 := match n with 0 => finite 1 | S p => cons (omega_tower p) 0 zero end.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List