proposition: Lemma af_left_sum (X Y : Type) (A : X -> X -> Prop) : @almost_full X A -> @almost_full (X+Y) (left_sum_lift A).
proof: Proof. intro afA. induction afA. apply AF_SUP; intro x. apply AF_SUP; intro y. apply AF_ZT. intros. destruct x; (repeat (auto; firstorder)). destruct y; (repeat (auto; firstorder)). destruct x0; (repeat (auto; firstorder)). destruct y; (repeat (auto; firstorder)). destruct x0; (repeat (auto; firstorder)). apply AF_SUP; intro x. destruct x. apply (af_strengthen (H0 x)). intros. destruct y; (repeat (auto; firstorder)). destruct x0; (repeat (auto; firstorder)). apply AF_SUP; intro z. destruct z. apply (af_strengthen (H0 x)). intros. destruct x0; (repeat (auto; firstorder)). destruct y0; (repeat (auto; firstorder)). apply AF_ZT. intros. destruct x; (repeat (auto; firstorder)). Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)