proposition: Lemma approx_ok alpha beta : forall fuel i j gamma, approx alpha beta fuel i = Some (j,gamma) -> gamma = canon alpha (S j) /\ lt beta gamma.
proof: Proof. induction fuel as [| f IHfuel ]. - cbn; discriminate. - intros i j gamma H0; cbn in H0. destruct (decide (lt beta (canon alpha (S i)))) as [H1|H1]. + injection H0; intros; subst; split;auto. + now specialize (IHfuel tt (S i) _ _ H0). Qed.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)