proposition: Lemma evalDet_step_app_done_eq : forall (A : Set)(c : Comp A) s s' s'' a, evalDet_step c s = (cs_done a s'') -> evalDet_step c (s ++ s') = (cs_done a (s'' ++ s')).
proof: Proof. induction c; intuition; simpl in *. inversion H; clear H; subst. trivial. case_eq (evalDet_step c s); intuition; rewrite H1 in H0; try discriminate. case_eq (shiftOut s n); intuition; rewrite H0 in H. destruct p. inversion H; clear H; subst. discriminate. discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia