proposition: Lemma phi_mono_weak_r : forall a b c, nf a -> nf b -> nf c -> b t2<= c -> phi a b t2<= phi a c.
proof: Proof. destruct 4. - subst c;left;auto with T2. - right; apply phi_mono_r;auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)