proposition: Theorem evalDet_done_eof_func: forall (A : Set) (c : Comp A) (a : A) (s : Blist), evalDet c s (ca_done a) -> evalDet c s (@ca_eof A) -> False.
proof: Proof. intuition. inversion H; clear H; subst. inversion H0; clear H0; subst. eapply evalDet_steps_done_eof_func; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia