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 (p,Asec) (q,Bsec). exists (oplus_binary p q). apply oplus_binary_sec_intersection; repeat auto. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)