proposition: Corollary af_sum_lift (X Y : Type) : forall (A : X -> X -> Prop) (B : Y -> Y -> Prop), almost_full A -> almost_full B -> almost_full (sum_lift A B).
proof: Proof. intros A B afA afB. assert (almost_full (fun x y => left_sum_lift A x y /\ right_sum_lift B x y)). apply af_intersection. apply af_left_sum. apply afA. apply af_right_sum. apply afB. apply (af_strengthen H). intros. destruct x; repeat firstorder. destruct y; repeat firstorder. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)