proposition: Lemma af_product_left (X Y : Type) (A:X->X->Prop) : almost_full A -> almost_full (fun (x:X*Y) (y:X*Y) => A (fst x) (fst y)).
proof: Proof. intros afA. apply (@af_cofmap _ _ (@fst X Y) A afA). Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)