fact: Fixpoint af_tree_iter {x : X} (accX : Acc R x) := match accX with | Acc_intro f => SUP (fun y => match decR y x with | left Ry => af_tree_iter (f y Ry) | right _ => ZT end) end.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)