fact: Fixpoint FueledFix (fuel : nat) (base : Comp R) (body : (A -> Comp R) -> A -> Comp R) (arg : A) : Comp R := match fuel with | O => base | S fuel' => body (FueledFix fuel' base body) arg end.
imports: Coq.Classes.Morphisms Coq.Classes.SetoidTactics Fiat.Computation