proposition: Lemma oplus_binary (X : Type): forall A, almost_full A -> forall B, almost_full B -> @almost_full X (fun x y => A x y /\ B x y).
proof: Proof. intros A afA. induction afA. intros B afB. apply (af_strengthen afB). intros. split. apply H. apply H0. intros B afB. induction afB. assert (almost_full R). apply AF_SUP; apply H. apply (af_strengthen H2). intros. split. apply H3. apply H1. apply AF_SUP; intro x0. apply oplus_unary_cor. assert (almost_full R0). apply AF_SUP; apply H1. apply (af_strengthen (H0 x0 R0 H3)). intros. destruct H4. destruct H4. left. auto. right. auto. apply (af_strengthen (H2 x0)). intros. destruct H3. destruct H4. left. auto. right. auto. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)