proposition: Lemma sort_nf : forall alpha, nfs alpha -> nf (sort alpha).
proof: Proof. induction alpha;simpl. constructor. intro; apply sort_aux_nf. inversion H;auto. apply IHalpha2. inversion H;auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0