proposition: Lemma evalDet_steps_app_eq : forall (A : Set)(c : Comp A) s s' s'' a, evalDet_steps (cs_more c s) (cs_done a s'') -> evalDet_steps (cs_more c (s ++ s')) (cs_done a (s'' ++ s')).
proof: Proof. intuition. eapply evalDet_steps_app_eq_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia