proposition: Lemma phi0_mono alpha beta : alpha o< beta -> E0_phi0 alpha o< E0_phi0 beta.
proof: Proof. destruct alpha, beta; unfold E0lt; cbn; auto with T1. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)