proposition: Lemma oplus_unary (X : Type) (A B : X -> Prop): forall R, almost_full R -> forall T, almost_full T -> forall C, (forall x y, R x y -> C x y \/ A x) -> (forall x y, T x y -> C x y \/ B x) -> almost_full (fun x y => C x y \/ (A x /\ B x)).
proof: Proof. intros R afR. induction afR. intros T afT C Req Teq. eapply af_strengthen. apply afT. intros. assert (C x y \/ B x). apply Teq; apply H0. assert (C x y \/ A x). apply Req; apply H. destruct H1. left; auto. destruct H2. left. auto. right; auto. intros T afT. induction afT. intros C Req Teq. assert (almost_full R). apply AF_SUP; apply H. eapply (af_strengthen H2). intros. assert (C x y \/ A x). apply Req; apply H3. assert (C x y \/ B x). apply Teq; apply H1. destruct H4. left. auto. destruct H5. left. auto. right; auto. intros C Req Teq. apply AF_SUP; intro x0. assert (almost_full (fun y z : X => ((C y z \/ A y /\ B y) \/ C x0 y) \/ A x0 /\ B x0)). eapply oplus_nullary_cor. assert (almost_full R0). apply AF_SUP. apply H1. remember (H0 x0 R0 H3 (fun x y => C x y \/ C x0 x \/ A x0)) as G0. clear HeqG0. clear H0. eapply af_strengthen. apply G0. intros. clear G0. clear H2. destruct H0. assert (C x y \/ A x). apply Req. apply H0. destruct H2. left. left. auto. right. auto. assert (C x0 x \/ A x0). apply Req. auto. destruct H2. left. right. left. auto. left. right. right. auto. intros. clear G0. clear H2. assert (C x y \/ B x). apply Teq. apply H0. destruct H2. left. left. auto. right. auto. intros. simpl in H0. destruct H0. destruct H0. left. left. left. auto. destruct H0. left. right. auto. right. auto. left. left. right. auto. clear H0. remember (H2 x0 (fun x y => C x y \/ C x0 x \/ B x0)) as G0. clear HeqG0. clear H2. eapply af_strengthen. apply G0. clear G0. intros. assert (C x y \/ A x). apply Req. apply H0. destruct H2. left. left. auto. right. auto. clear G0. intros. destruct H0. assert (C x y \/ B x). apply Teq. apply H0. destruct H2. left. left. auto. right. auto. assert (C x0 x \/ B x0). apply Teq. apply H0. destruct H2. left. right. left. auto. left. right. right. auto. intros. simpl in H0. destruct H0. destruct H0. left. left. left. auto. destruct H0. left. right. auto. right. auto. left. left. right. auto. apply (af_strengthen H3). intros. destruct H4. destruct H4. destruct H4. left. left. auto. left. right. auto. right. left. auto. right. right. auto. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)