Library epsilon0.MSE0

Add LoadPath "../prelude".
Add LoadPath "../rpo".

Require Import Arith.
Require Import ArithRing.

Require Import More_nat.
Require Import EPSILON0.

Inductive nfs : T1 -> Prop :=
|nfs_nil : nfs zero
|nfs_cons : forall a n b, nf a -> nfs b -> nfs (cons a n b).

Hint Constructors nfs nf : T1.

Lemma nf_nfs : forall a, nf a -> nfs a.
Proof.
 induction 1; simpl; auto with T1.
Qed.

Fixpoint multiplicity (c:T1) (a:T1) {struct a}: nat :=
  match a with
  | zero => 0
  | (cons a' n' b') =>
      match T1_eq_dec c a' with
      | left _ => ( (S n') +(multiplicity c b'))%nat
      | right _ => multiplicity c b'
      end
  end.

Lemma multiplicity_rw1 : forall a n b, multiplicity a (cons a n b) =
                                  (S n + multiplicity a b)%nat.
  simpl.
 intros; case (T1_eq_dec a a).
 auto.
 intro; absurd (a=a);auto.
Qed.

Lemma multiplicity_rw2 : forall a a' n' b', a <> a' ->
                         multiplicity a (cons a' n' b') = multiplicity a b'.
Proof.
 simpl.
 intros; case (T1_eq_dec a a').
 intro; case H;auto.
 auto.
Qed.

Fixpoint app (o o':T1) {struct o} : T1 :=
  match o with zero => o'
             | cons a n b => cons a n (app b o')
  end.

Infix "::" := app (at level 60, right associativity) : cantor_scope.

Lemma multiplicity_of_app : forall l l' a, multiplicity a (l :: l') =
                                     (multiplicity a l + multiplicity a l')%nat.
Proof.
 induction l; simpl; auto with arith.
 intros.
 case (T1_eq_dec a l1).
 rewrite IHl2.
 clear IHl1 IHl2; intro; omega.
 auto.
Qed.

Definition equiv (l l':T1) :=
    forall o, multiplicity o l = multiplicity o l'.

Lemma equiv_refl : forall l:T1, equiv l l.
Proof.
 unfold equiv; trivial.
Qed.

Lemma equiv_sym : forall l l':T1, equiv l l' -> equiv l' l.
Proof.
  unfold equiv; auto.
Qed.

Lemma equiv_trans :
 forall l l' l'', equiv l l' ->
                         equiv l' l'' ->
                         equiv l l''.
Proof.
 intros l l' l'' H H0 z.
 eapply trans_eq; eauto.
Qed.

Lemma equiv_cons :
 forall a n l l', equiv l l' ->
                  equiv (cons a n l) (cons a n l').
Proof.
 intros a n l l' H a'.
 simpl ; case (T1_eq_dec a' a); auto.
Qed.

Lemma equiv_tail : forall a n l l', equiv (cons a n l) (cons a n l') ->
                                     equiv l l'.
Proof.
 intros.
 unfold equiv;intros.
 generalize (H o).
 simpl.
 case (T1_eq_dec o a).
 intro;omega.
 auto.
Qed.

Lemma equiv_perm :
 forall a n b p l l',
   equiv l l' ->
   equiv (cons a n (cons b p l))(cons b p (cons a n l')).
Proof.
 intros a n b p l l' H c; simpl.
 case (T1_eq_dec c a); case (T1_eq_dec c b);
  simpl; case (H c); auto.
 intros;ring_nat.
Qed.

Lemma app_equiv_comm : forall l l', equiv (l :: l') (l' :: l).
 unfold equiv;intros.
 do 2 rewrite multiplicity_of_app.
 auto with arith.
Qed.

Lemma app_equiv_assoc : forall l l' l'', equiv ((l ::l') :: l'')
                                           (l :: (l' :: l'')).
 unfold equiv;intros.
 repeat rewrite multiplicity_of_app.
  auto with arith.
Qed.


Lemma equiv_cong1 : forall l1 l2 l, equiv l1 l2 -> equiv (l1 :: l)
                                                         (l2 :: l).

 unfold equiv;intros;repeat rewrite multiplicity_of_app.
 auto with arith.
Qed.

 Lemma equiv_cong2 : forall l1 l2 l, equiv l1 l2 -> equiv (l :: l1)
                                                          (l :: l2).

 unfold equiv;intros;repeat rewrite multiplicity_of_app.
 auto with arith.
Qed.

Hint Resolve equiv_cons equiv_refl equiv_perm equiv_tail app_equiv_assoc : T1.

Fixpoint sort_aux (a:T1)(n:nat) (l:T1) {struct l} : T1 :=
  match l with
  | zero => (cons a n zero)
 | cons b p l' =>
     ( match trichotomy_inf a b with
      | inleft (left _ ) => (cons b p (sort_aux a n l'))
      | inleft (right _) => (cons b (S n +p)%nat l')
      | inright _ => (cons a n (cons b p l'))
      end)
   end.

Lemma sort_aux_equiv : forall l a n,
                  equiv (cons a n l) (sort_aux a n l).
Proof.
 induction l ; auto with T1.
 intros x n0; simpl. case (trichotomy_inf x l1).

 destruct s.
 eapply equiv_trans.
 2:eapply equiv_cons.
 apply equiv_perm.
 apply equiv_refl.
 auto.
 subst l1.
 2:intro;apply equiv_refl.
 unfold equiv;simpl.
 intro o;case (T1_eq_dec o x).
 intro; omega.
 auto.
Qed.

Lemma sort_aux_nf :
 forall (l x:T1) n, nf x -> nf l -> nf (sort_aux x n l).
Proof.
 induction 2.

 simpl.
 auto with T1.

 simpl.
 case (trichotomy_inf x a).
 destruct s.
 constructor;auto.
 constructor; auto with T1.
 constructor; auto with T1 arith.
  constructor; auto with T1 arith.
 simpl.
case (trichotomy_inf x a).
destruct s.
simpl in IHnf2.
generalize IHnf2.
case (trichotomy_inf x a').
destruct s.
constructor 3.
 auto.
 auto.
auto.

subst x.
 constructor;auto.
 constructor;auto.
 constructor;auto.
constructor.
auto.
auto.
 constructor;auto.
Qed.

Fixpoint sort (alpha :T1) : T1 :=
 match alpha with zero => zero
            | cons a n b => sort_aux a n (sort b)
 end.

Lemma sort_equiv :
  forall alpha:T1, equiv alpha (sort alpha).
Proof.
 induction alpha;simpl.
 split;auto with T1.
 apply equiv_trans with (cons alpha1 n (sort alpha2)).
 apply equiv_cons.
 auto.
 apply sort_aux_equiv.
Qed.

Lemma sort_nf : forall alpha, nfs alpha -> nf (sort alpha).
Proof.
 induction alpha;simpl.
 constructor.
 intro; apply sort_aux_nf.
 inversion H;auto.
 apply IHalpha2.
 inversion H;auto.
Qed.

Definition ltM (a:T1)(l l':T1) :=
 (multiplicity a l < multiplicity a l')%nat /\
 forall b, a < b -> multiplicity b l = multiplicity b l'.

Lemma ltM_equiv_ltM : forall a l l' l'', ltM a l l' ->
                                         equiv l' l'' -> ltM a l l''.
Proof.
 unfold ltM, equiv.
 intros.
 case H; intros; clear H.
 split.
 rewrite <- H0; auto.
 intros; rewrite <- H0;auto.
Qed.

Lemma ltM_equiv_ltMR :
  forall a l l' l'', ltM a l l' -> equiv l l'' -> ltM a l'' l'.
Proof.
 unfold ltM, equiv.
 intros.
 case H; intros; clear H.

 split.

 rewrite <- H0; auto.
 intros; rewrite <- H0;auto.
Qed.

Lemma ltM_trans : forall a l l' , ltM a l l' -> forall l'', ltM a l' l'' ->
                                                            ltM a l l''.
 induction 1.
 destruct 1.
 split.
 eauto with arith.
 intros ; rewrite H0; auto.
 Qed.

Lemma ltM_trans_1 : forall a b l l' l'', a < b -> ltM a l l' ->
                                          ltM b l' l'' ->
                                          ltM b l l''.
 destruct 2.
 destruct 1.
 split.
 replace (multiplicity b l) with (multiplicity b l').
 auto.
 symmetry;apply H1; auto.
 intros; transitivity (multiplicity b0 l');auto.
 apply H1.
 eapply lt_trans; eauto.
Qed.

Lemma ltM_trans_2 : forall a b l l' l'', b < a -> ltM a l l' ->
                                          ltM b l' l'' ->
                                          ltM a l l''.
 destruct 2.
 destruct 1.
 split.
 replace (multiplicity a l'') with (multiplicity a l').
 auto.
 apply H3.
 auto.
 intros;
 transitivity (multiplicity b0 l');auto.
 apply H3.
 eapply lt_trans; eauto.
Qed.

 Lemma lt_ltM : forall a n b l l', b < a -> ltM a l l' ->
                                     ltM a (cons b n l) l'.
 induction 2; split.
 simpl.
 case (T1_eq_dec a b).
 intro; absurd (lt a a);auto with T1.
 subst b;auto.
 auto.
 intros; simpl.
 case (T1_eq_dec b0 b).
 intro; subst b0; case (lt_not_gt H);auto.
 auto.
 Qed.

Lemma nf_multiplicity_head : forall l c n , nf (cons c n l) ->
                                          multiplicity c (cons c n l) = S n.
Proof.
 induction l.
 simpl.
 intros; case (T1_eq_dec c c).
 auto with arith.
 intros; absurd (c=c); auto.
 intros;case (T1_eq_dec c c).
 2: intros;absurd (c=c);auto.
 case (T1_eq_dec c l1); simpl.
 assert (c <> l1).
 red; intro; subst l1.
 case (lt_irr (a:=c)).
 inversion_clear H;auto.
 intros; absurd (c=l1);auto.
 assert (nf (cons c n0 l2)).
 generalize H;induction l2.
 constructor.
 inversion H;auto.
 constructor.
 inversion H;auto.
 apply lt_trans with l1;auto.
 inversion H8;auto.
 inversion H0;auto.
 inversion H0.
 inversion H8;auto.
 intros; case (T1_eq_dec c c).
 case (T1_eq_dec c l1).
 intro;case n1;auto.
 replace (multiplicity c l2) with 0.
 auto with arith.
 generalize H0;elim l2.
 simpl;auto.
 intros.
 simpl.
 case (T1_eq_dec c t).
 intro.
 subst t; inversion H3.
 case (lt_irr H7).
 intro;apply H2.
 generalize H3;case t0.
 constructor;auto.
 inversion H3;auto.
 constructor;auto.
 inversion H4.
 apply lt_trans with t;auto.
 inversion H12;auto.
 inversion H4;auto.
 inversion H4.
 inversion H12;auto.
 intro H1;case H1;auto.
Qed.

Lemma nf_multiplicity_tail : forall l a c n ,
                                 a < c -> nf (cons c n l) ->
                                 multiplicity a (cons c n l) = multiplicity a l.
Proof.
 inversion_clear 2.
 simpl;case (trichotomy_inf a c).
 destruct 1.
 case (T1_eq_dec a c).
 intro; subst a; absurd (lt c c);auto with T1.
 auto.
 case (T1_eq_dec a c).
 intro; subst a; absurd (lt c c);auto with T1.
 auto .

 case (T1_eq_dec a c).
   intro; subst a; absurd (lt c c);auto with T1.
 auto.
 simpl.
  case (T1_eq_dec a c).
 case (T1_eq_dec a a').
   intro; subst a; intros;absurd (lt c c);auto with T1.
 subst c;auto.
  intros; subst a; intros;absurd (lt c c);auto with T1.
  auto.
Qed.

Lemma nf_multiplicity_big : forall l a c n , c < a -> nf (cons c n l) ->
                                                 multiplicity a (cons c n l) = 0.

Proof.
 induction l.
 inversion_clear 2.
 simpl; case (T1_eq_dec a c).
 intros; subst a; intros;absurd (lt c c);auto with T1.
 auto.
 simpl.
 intros.
 case (T1_eq_dec a c).
 intros; subst a; intros;absurd (lt c c);auto with T1.
 intro;
 case (T1_eq_dec a c).
 intro; subst a.
 case (lt_irr H);auto.
intros; case (T1_eq_dec a l1).
intro; absurd (lt a l1).
rewrite <- e.
subst l1.
apply lt_irr.
subst l1.
inversion_clear H0;auto.
eapply lt_trans;eauto.
generalize (IHl2 a c n H).
simpl.
case (T1_eq_dec a c).
intro; absurd (a=c);auto.
intros.
apply H1.
inversion_clear H0.
auto.
inversion_clear H4.
constructor;auto.
constructor; auto.
eapply lt_trans ; eauto.
Qed.

Lemma ltM_inv : forall a b n l l',
  nf (cons b n l) -> nf (cons b n l') ->
  ltM a (cons b n l) (cons b n l') ->
                    ltM a l l'.
Proof.
 inversion_clear 3.
 case (trichotomy_inf a b).
 destruct 1.
 do 2 rewrite nf_multiplicity_tail in H2; auto.
 split;auto.
 intros.
 generalize (H3 _ H1).
 simpl.
 case (T1_eq_dec b0 b).
 auto.
 clear H3;intro;omega.
 auto.
 subst b; do 2 rewrite nf_multiplicity_head in H2;auto.
 absurd (n<n)%nat; auto with arith.
 intro.
 do 2 rewrite nf_multiplicity_big in H2;auto.
 inversion H2.
Qed.

Lemma ltM_inv2 : forall l l' a b n b' n', nf (cons b n l) ->
                                       nf (cons b' n' l') ->
                                       ltM a (cons b n l) (cons b' n' l') ->
                                         a <= b'.
intros.
case H1.
intros H2 H3.
case (trichotomy_inf a b').
destruct 1.
auto.
auto.
right;auto.
left;auto.
intro.
rewrite (nf_multiplicity_big _ _ _ _ l0 H0) in H2;auto.
inversion H2.
Qed.

Lemma ltM_inv3: forall l l' a b n b' n', a < b' ->
                                         nf (cons b n l) ->
                                         nf (cons b' n' l') ->
                                         ltM a (cons b n l) (cons b' n' l') ->
                                          b = b' /\ n = n'.
intros.
case H2.
intros.
case (trichotomy_inf b b').
destruct 1.
generalize (H4 _ H).
rewrite nf_multiplicity_big;auto.
rewrite nf_multiplicity_head.
discriminate 1.
auto.
split.
auto.
subst b'.
generalize (H4 _ H).
rewrite nf_multiplicity_head ;auto.
rewrite nf_multiplicity_head ;auto.
intro.
assert (lt a b).
eapply lt_trans;eauto.
generalize (H4 _ H5).
rewrite nf_multiplicity_head ;auto.
rewrite nf_multiplicity_big ;auto.
intro;absurd (0<n)%nat.
discriminate H6.
discriminate H6.
Qed.

Lemma ltM_cons : forall a l l' b n, ltM a l l' -> ltM a (cons b n l)
                                                         (cons b n l').
Proof.
 intros.
 unfold ltM.
 case H; intros.
 split; simpl.
 case (T1_eq_dec a b).
 auto with arith.
 auto.
 intros; case (T1_eq_dec b0 b).
 intro; subst b0;auto.
 intro;apply H1.
auto.
Qed.

Lemma ltM_app : forall a l l' l'', ltM a l l' -> ltM a (l'' :: l)
                                                       (l'' :: l').
Proof.
 induction l'';simpl.
 auto.
 intros;apply ltM_cons.
 auto.
Qed.

Lemma ltM_appR : forall a l l' l'', ltM a l l' -> ltM a (app l l'')
                                                        (app l' l'').
Proof.
  intros.
  eapply ltM_equiv_ltM.
  2:apply app_equiv_comm.
  eapply ltM_equiv_ltMR.
  2:apply app_equiv_comm.
 apply ltM_app.
 auto.
Qed.

Lemma lt_ltM2 : forall c c', nf c -> nf c' ->
                             c < c' ->
                            {a:T1| ltM a c c'}.
Proof.
 induction c; destruct c'.
 intros; elimtype False.
 inversion H1.
 exists c'1;simpl.
 constructor.
 simpl.
 case (T1_eq_dec c'1 c'1).
 auto with arith.
 intros; absurd (c'1=c'1);auto.
 intros;rewrite nf_multiplicity_big.
 simpl;auto.
 auto.
 auto.
 intros;elimtype False.
inversion H1.
intros.
case (trichotomy_inf c1 c'1).
destruct 1.

exists c'1.
simpl.
inversion H1.
split.

rewrite nf_multiplicity_big.
rewrite nf_multiplicity_head.
auto with arith.
 auto.
 auto.
 auto.
intros; repeat rewrite nf_multiplicity_big.
auto.
auto.
auto.
eapply lt_trans;eauto.
 auto.
 split.
 repeat rewrite nf_multiplicity_head.
 auto with arith.
 auto.
 subst c'1.
 auto.
intros.

repeat rewrite nf_multiplicity_big;auto.
subst c'1;auto.
subst c'1; case (lt_irr l).
subst c'1.

case (lt_eq_lt_dec n n0).
destruct 1.
exists c1.
split.
repeat rewrite nf_multiplicity_head.
auto with arith.
auto.
auto.
intros; repeat rewrite nf_multiplicity_big;auto.
subst n0.
assert (lt c2 c'2).
eapply lt_inv_b;eauto.

case (IHc2 c'2).
eapply nf_inv2;eauto.

eapply nf_inv2;eauto.
auto.
intros;exists x.
apply ltM_cons.
auto.
intros.
elimtype False.
 generalize (lt_inv_nb H1).
destruct 1.
absurd (n<n)%nat;eauto with arith.
case H2;intros ;subst n.
absurd (n0<n0)%nat;auto with arith.
intros.
absurd (EPSILON0.le c1 c'1).
unfold EPSILON0.le.
red; destruct 1.
subst c'1;case (lt_irr l).
case (lt_not_gt l);auto.
inversion H1.
right;auto.
subst c1;left;auto.
left.
auto.
Qed.

Lemma ltM_lt : forall a l l', nf l -> nf l' ->
                          ltM a l l' ->
                          l < l'.
Proof.
 induction l; destruct l'.
 intros; absurd (ltM a zero zero);auto.
 unfold ltM;simpl.
 red; case 1.
 destruct 2.
 inversion H2.
 simpl.
 auto with T1.
 inversion 3.
 inversion H2.
 intros.
 case (trichotomy_inf l1 l'1).
 destruct 1.
 constructor 2;auto.
 subst l'1.
 case (trichotomy_inf a l1).
 destruct 1.
 case H1;intros.
 rewrite (nf_multiplicity_tail _ _ _ _ l H) in H2.
 rewrite (nf_multiplicity_tail _ _ _ _ l H0) in H2.
 generalize (H3 _ l).
 rewrite nf_multiplicity_head .
 rewrite nf_multiplicity_head .
 injection 1.
 intro; subst n0.
 constructor 4.
 apply IHl2.
 inversion_clear H; eauto.
 constructor.
 inversion_clear H0; eauto.
 constructor.
 split.
 auto.
 intros b H11.
 generalize (H3 _ H11).
 simpl.
 case (T1_eq_dec b l1).
 intros; clear H3; omega.
 auto.
 auto.
 auto.
 subst l1.
 case H1;intros.
 do 2 rewrite nf_multiplicity_head in H2.
 constructor 3;auto.
 clear H3;omega.
 auto.
 auto.
 auto.
 case H1;intros.
 do 2 rewrite nf_multiplicity_big in H2.
 inversion_clear H2.
 auto.
 auto.
 auto.
 auto.
 auto.
 auto.
 auto.
 auto.
 intro.
 generalize (ltM_inv2 _ _ _ _ _ _ _ H H0 H1).
 destruct 1.
 subst l'1.
 case H1;intros.
 generalize (H3 _ l).
 rewrite (nf_multiplicity_head);auto.
 rewrite (nf_multiplicity_big);auto.
 intro.
 discriminate H4.
 generalize (ltM_inv3 _ _ _ _ _ _ _ H2 H H0 H1).
 destruct 1.
 subst l'1.
 case (lt_irr l).
Qed.


Lemma ltM_tail : forall a n l, ltM a l (cons a n l).
Proof.
 intros; unfold ltM.
 split.
 simpl.
 case (T1_eq_dec a a).
 intro; omega.
 intro; absurd (a=a);auto.
 intros; simpl.
 case (T1_eq_dec b a).
 intro; absurd (lt a b).
subst b;auto with T1.
 auto.
 auto.
Qed.

Lemma ltM_head : forall a n a' p l , a' < a ->
                                     ltM a (cons a' p l)
                                           (cons a n l).
Proof.
 intros; unfold ltM.
 split.
 simpl.
 case (T1_eq_dec a a').
 intro.
 absurd (lt a a);auto with T1.
 subst a;auto.
 case (T1_eq_dec a a).
 intros;omega.
 intros; absurd (a=a);auto.
 simpl.
 intros;case (T1_eq_dec b a'); case (T1_eq_dec b a).
 intro; subst b; absurd (lt a a);auto with T1.
 intros.
 subst b; case (lt_not_gt H0);auto.
 intro; subst b; absurd (lt a a);auto with T1.
 auto.
Qed.

Lemma nfs_to_nf : forall l a, nfs l -> (0 < multiplicity a l)%nat -> nf a.
Proof.
  induction l.
  simpl.
  inversion 2.
  simpl.
  intros; case (T1_eq_dec a l1).
  intro; subst a.
  inversion H;auto.
  generalize H0; case (T1_eq_dec a l1).
  intros; absurd (a=l1);auto.
  intros.
  apply IHl2.
  inversion H.
  auto.
  auto.
 Qed.

Lemma nf_to_nfs : forall l, nf l ->
                       nfs l.
Proof.
  induction l.
  constructor.
  constructor.
  inversion H;auto.
  inversion H;auto.
  constructor.
  subst l2.
  auto.
 Qed.

Lemma nf_unicity :forall l, nf l -> forall l',equiv l l' -> nf l' -> l=l'.
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.