proposition: Corollary af_intersection (X : Type) (A B :X->X->Prop): almost_full A -> almost_full B -> almost_full (fun x y => A x y /\ B x y).
proof: Proof. intros. apply oplus_binary. apply H. apply H0. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)