proposition: Lemma af_bool : almost_full (@eq bool).
proof: Proof. apply AF_SUP. intro x. apply AF_SUP. intro y. apply AF_SUP. intro z. apply AF_ZT. intros. destruct x. destruct y. firstorder. firstorder. destruct z. firstorder. firstorder. destruct y. firstorder. destruct z. firstorder. firstorder. firstorder. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)