proposition: Lemma evalDet_app_eq : forall (A : Set)(c : Comp A) s s' a, evalDet c s (ca_done a) -> evalDet c (s ++ s') (ca_done a).
proof: Proof. intuition. inversion H; clear H; subst. econstructor. eapply evalDet_steps_app_eq. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia