proposition: Lemma evalDet_steps_done_func_h : forall (A : Set)(x : comp_state A) y1, evalDet_steps x y1 -> forall a a' s s', y1 = (cs_done a s) -> evalDet_steps x (cs_done a' s') -> (a = a' /\ s = s').
proof: Proof. induction 1; intros; subst. inversion H0; clear H0; subst. intuition. inversion H2; clear H2; subst. eapply IHevalDet_steps; trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia