proposition: Lemma nf_unicity :forall l, nf l -> forall l',equiv l l' -> nf l' -> l=l'.
proof: Proof. induction 1. induction 2. auto. unfold equiv in H. generalize (H a). simpl. case (T1_eq_dec a a). discriminate 2. intros; absurd (a=a);auto. unfold equiv in H. generalize (H a). simpl. case (T1_eq_dec a a). discriminate 2. intros; absurd (a=a);auto. destruct l'. unfold equiv . intro H0;generalize (H0 a). simpl. case (T1_eq_dec a a). discriminate 2. intros; absurd (a=a);auto. case l'2. unfold equiv; simpl. intros. generalize (H0 a). case (T1_eq_dec a a). case (T1_eq_dec a l'1). intros. subst l'1. assert (n=n0). clear H0;omega. subst n;auto. discriminate 3. intro; absurd (a=a);auto. unfold equiv. intros. generalize (H0 l'1). simpl. case (T1_eq_dec l'1 a). intro;subst l'1. case (T1_eq_dec a a). case (T1_eq_dec a t). intros;subst t. absurd (lt a a). apply lt_irr. inversion_clear H1;auto. intros. generalize (H0 t). simpl. case (T1_eq_dec t a). intro; absurd (t = a);auto. case (T1_eq_dec t t). discriminate 3. intro; absurd (t=t);auto. intro;absurd (a=a);auto. case (T1_eq_dec l'1 l'1). discriminate 3. intro;absurd (l'1 = l'1);auto. destruct l'. unfold equiv. intros. generalize (H2 a);simpl. case (T1_eq_dec a a). discriminate 2. intro;absurd (a=a);auto. case l'2. unfold equiv;intros . generalize (H2 a). simpl. case (T1_eq_dec a a). case (T1_eq_dec a a'). intros;subst a'. case (lt_irr H). case (T1_eq_dec a l'1). intro; subst l'1. generalize (H2 a'). simpl. case (T1_eq_dec a' a). intro; absurd (a'=a);auto. subst a'. case (lt_irr H). case (T1_eq_dec a' a'). discriminate 3. intro;absurd (a'=a');auto. discriminate 4. intro;absurd (a=a);auto. intros. case (trichotomy_inf a l'1). destruct 1. unfold equiv in H2. generalize (H2 l'1). rewrite nf_multiplicity_big. rewrite nf_multiplicity_head. discriminate 1. auto. auto. constructor;auto. subst l'1. unfold equiv in H2. generalize (H2 a). rewrite nf_multiplicity_head. rewrite nf_multiplicity_head. injection 1;intro; subst n0. rewrite (IHnf2 (cons t n1 t0)). auto. apply equiv_tail with a n. unfold equiv;auto. inversion H3;auto. auto. constructor;auto. intros. generalize (H2 a). rewrite nf_multiplicity_head. rewrite nf_multiplicity_big. discriminate 1. auto. auto. constructor;auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0