proposition: Corollary af_from_wf : almost_full (fun x y => not (R y x)).
proof: Proof. exists (SUP af_tree). apply secure_from_wf. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)