proposition: Corollary af_union: forall (X:Type) (A:X->X->Prop) (B:X->X->Prop), almost_full A -> almost_full (fun x y => A x y \/ B x y).
proof: Proof. intros X A B (p,Asec). exists p. apply sec_union. apply Asec. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)