fact: Fixpoint approx alpha beta fuel i := match fuel with FO => None | Fuel.FS f => let gamma := canon alpha (S i) in if decide (lt beta gamma) then Some (i,gamma) else approx alpha beta (f tt) (S i) end.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)