proposition: Lemma evalDet_repeat_steps_app_nil : forall (A : Set)(c : Comp A) P ls1 ls2 b a, evalDet_repeat_steps P (cs_more c ls1) (cs_eof A) -> evalDet_repeat_steps P (cs_more c (ls1 ++ b :: nil)) (cs_done a ls2) -> (forall s s' b a, evalDet_steps (cs_more c s) (cs_eof A) -> evalDet_steps (cs_more c (s ++ b :: nil)) (cs_done a s') -> s' = nil) -> ls2 = nil.
proof: Proof. intuition. eapply evalDet_repeat_steps_app_nil_h. eapply H. eauto. trivial. eauto. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia