proposition: Lemma cons_unicity : forall a n b a' n' b', nf (cons a n b) -> nf (cons a' n' b') -> (omega^a)*(F (S n))+b = (omega^a')*(F (S n'))+b' -> a=a' /\ n = n' /\ b = b'.
proof: Proof. intros a n b a' n' b' N N'. rewrite <- (cons_ambiguity N). rewrite <- (cons_ambiguity N'). injection 1;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List