proposition: Lemma R1_decrease : forall u h h', R1 u h h' -> h2o h' < h2o h.
proof: Proof. induction 1. simpl. auto with T1. simpl. generalize (S1_decrease u l l' s). destruct 1. generalize (sort_equiv (h2ol l)). intro He. generalize (sort_equiv (h2ol l')). intro He'. generalize (sort_nf (h2ol l)). intro Hs. generalize (sort_nf (h2ol l')). intro Hs'. apply ltM_lt with x ; auto. apply sort_nf. apply h2ol_nfs. apply sort_nf. apply h2ol_nfs. eapply ltM_equiv_ltM. 2:eauto. eapply ltM_equiv_ltMR. eauto. auto. Qed.
imports: Arith Omega List EPSILON0 MSE0