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 (p,Asec) (q,Bsec). exists (oplus_binary (left_sum_tree Y p) (right_sum_tree X q)). apply sec_sum_lift; repeat assumption. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)