proposition: Lemma af_product (X : Type) (Y : Type) : forall (A : X -> X -> Prop) (B : Y -> Y -> Prop), almost_full A -> almost_full B -> almost_full (fun x y => A (fst x) (fst y) /\ B (snd x) (snd y)).
proof: Proof. intros A B afA afB. apply(af_intersection (@af_cofmap _ _ (@fst X Y) A afA) (@af_cofmap _ _ (@snd X Y) B afB)). Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)