fact: Definition af_tree : X → WFT := fun x => af_tree_iter (wfR x).
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)