proposition: Lemma af_right_sum (X Y : Type) (B : Y -> Y -> Prop) : @almost_full Y B -> @almost_full (X+Y) (right_sum_lift B).
proof: Proof. intros. unfold right_sum_lift. eapply af_cofmap. apply af_left_sum. apply H. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)