proposition: Theorem evalDet_steps_done_eof_func : forall (A : Set) x (a : A) s, evalDet_steps x (cs_done a s) -> evalDet_steps x (@cs_eof A) -> False.
proof: Proof. intros. eapply evalDet_steps_done_eof_func_h. eapply H. eauto. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia