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