proposition: Lemma evalDet_steps_app_eq_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (c : Comp A) s s' s'' a, x = (cs_more c s) -> y = (cs_done a s'') -> evalDet_steps (cs_more c (s ++ s')) (cs_done a (s'' ++ s')).
proof: Proof. induction 1; intuition; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. econstructor. eapply evalDet_step_app_done_eq. eauto. econstructor. econstructor. eauto. erewrite evalDet_step_app_more_eq. eapply IHevalDet_steps. eauto. trivial. auto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia