proposition: Lemma evalDet_dec : forall (A : Set)(c : Comp A)(s : Blist), well_formed_comp c -> (exists a, evalDet c s (ca_done a)) \/ (evalDet c s (@ca_eof A)).
proof: Proof. intuition. edestruct (@evalDet_steps_dec _ c). trivial. destruct H0. destruct H0. left. econstructor. econstructor. eauto. right. econstructor. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia