fact: Fixpoint succ (c:T1) : T1 := match c with zero => finite 1 | cons zero n _ => cons zero (S n) zero | cons a n b => cons a n (succ b) end.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List