proposition: Lemma oplus_unary_cor (X : Type) (A B : X -> Prop) (C : X -> X -> Prop): almost_full(fun x y => C x y \/ A x) -> almost_full(fun x y => C x y \/ B x) -> almost_full (fun x y => C x y \/ (A x /\ B x)).
proof: Proof. intros. apply oplus_unary with (R := fun x y => C x y \/ A x) (T := fun x y => C x y \/ B x). apply H. apply H0. intros. apply H1. intros. apply H1. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)