proposition: Lemma oplus_nullary (X : Type) (A B : Prop) (R : X -> X -> Prop) : almost_full R -> forall C, (forall x y, R x y <-> C x y \/ A) -> almost_full (fun (x:X) (y:X) => C x y \/ B) -> almost_full (fun (x:X) (y:X) => C x y \/ A /\ B).
proof: Proof. intro afR. induction afR. intros. eapply af_strengthen. apply H1. intros. simpl in H2. destruct H2. left. auto. assert (C x y \/ A). apply H0. apply H. destruct H3. left. auto. right. auto. intros. apply AF_SUP. intro x. eapply af_strengthen. eapply H0 with (x := x) (C := fun y z => C x y \/ C y z). intros. split. intros. destruct H3. remember (H1 x0 y). destruct i. destruct (o H3). left. right. apply H4. right. apply H4. destruct (H1 x x0). destruct (H4 H3). left. left. apply H6. right. apply H6. intros. destruct H3. destruct H3. destruct (H1 x x0). firstorder. destruct (H1 x0 y). left. apply H5. left. apply H3. destruct (H1 x0 y). left. apply H5. right. apply H3. eapply af_strengthen. apply H2. intros. simpl in H3. destruct H3. left. right. apply H3. right. apply H3. intros. simpl in H3. destruct H3. destruct H3. right. left. apply H3. left. left. apply H3. right. right. apply H3. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)