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