proposition: Corollary af_from_wf (X:Type) (R : X -> X -> Prop) : well_founded R -> dec_rel R -> almost_full (fun x y => ~ R y x).
proof: Proof. intros. apply AF_SUP. intro x. assert (Acc R x). apply H. remember (@af_iter X R X0 x H0). clear Heqa. eapply af_strengthen. apply a. intros. simpl in H1. destruct H1. right; assumption. left; assumption. Defined.
imports: Coq(Arith Relations)