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 wfR decR. unfold almost_full. exists (SUP (af_tree wfR decR)). apply secure_from_wf. Defined.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)