proposition: Lemma evalDet_step_done_inv : forall (A : Set)(c : Comp A) a ls ls', evalDet_step c ls = cs_done a ls' -> exists eqd, c = Ret eqd a.
proof: Proof. intuition. destruct c; simpl in *. inversion H; clear H; subst. econstructor; eauto. case_eq (evalDet_step c ls); intuition; rewrite H0 in H; discriminate. destruct (shiftOut ls n). destruct p. discriminate. discriminate. discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia