proposition: Theorem lub_mono : forall (P Q :T2 -> Prop) l l', (forall o, nf o -> P o -> Q o) -> lub P l -> lub Q l' -> l t2<= l'.
proof: Proof. intros P Q l l' H (H1,(H2,H3)) (H'1,(H'2,H'3)). 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)