proposition: Lemma sorted_lt_lt_2 l alpha : sorted (cons alpha l) -> eval (cons alpha l) < phi0 (succ alpha).
proof: Proof. intros;apply (sorted_lt_lt H). inversion H;intros;eauto with schutte. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)