proposition: Lemma af_iter : forall (X:Type) (R : X -> X -> Prop) (decR : dec_rel R) (x:X) (accX : Acc R x), almost_full (fun y z => ~ R y x \/ ~ R z y).
proof: Proof. intros. induction accX. apply AF_SUP; intro y. destruct (decR x y). apply AF_ZT. intros. right. left. apply n. assert (almost_full (fun y0 z => ~ R y0 y \/ ~ R z y0)). apply H0. apply r. eapply af_strengthen. apply H1. intros. simpl in H2. destruct H2. right. right. auto. left. right. auto. Defined.
imports: Coq(Arith Relations)