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 <= l'.
proof: Proof. intros P Q l l' H (H1,(H2,H3)) (H'1,(H'2,H'3)). auto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo