proposition: Corollary af_union: forall (X : Type) (A B : X -> X -> Prop), almost_full A -> almost_full (fun x y => A x y \/ B x y).
proof: Proof. intros X A B afA. eapply af_strengthen. apply afA. auto. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)