proposition: Lemma sort_equiv : forall alpha:T1, equiv alpha (sort alpha).
proof: 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.
imports: Arith Omega ArithRing More_nat EPSILON0