proposition: Corollary af_cofmap (X Y:Type) (f:Y->X) (R:X->X->Prop): almost_full R -> almost_full (fun x y => R (f x) (f y)).
proof: Proof. intro afR. induction afR. apply AF_ZT. intros. apply H. apply AF_SUP. intro y. apply H0. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)