proposition: Lemma af_strengthen: forall (X:Type) (A : X -> X -> Prop), almost_full A -> forall (B : X -> X -> Prop), (forall x y, A x y -> B x y) -> almost_full B.
proof: Proof. intros X A p. induction p. intros. apply AF_ZT; auto. intros. apply AF_SUP. intro x. apply H0 with (x := x). intros. destruct H2. left; auto. right; auto. Defined.
imports: Coq(Arith Relations)