proposition: Lemma evalDet_steps_eof_inv : forall (A : Set)(c : Comp A) s, evalDet_steps (cs_more c s) (@cs_eof A) -> exists c'' s'', evalDet_steps (cs_more c s) (cs_more c'' s'') /\ evalDet_step c'' s'' = (@cs_eof A).
proof: Proof. intuition. eapply evalDet_steps_eof_inv_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia