proposition: Lemma evalDet_repeat_steps_nil_inv_h : forall (A : Set) P (x y : comp_state A), evalDet_repeat_steps P x y -> forall (P : A -> bool) c a ls', x = (cs_more c nil) -> y = (cs_done a ls') -> ls' = nil.
proof: Proof. induction 1; intuition; subst. inversion H2; clear H2; subst. inversion H3; clear H3; subst. eapply evalDet_steps_done_nil_inv. eauto. discriminate. inversion H4; clear H4; subst. assert (s' = nil). eapply evalDet_steps_done_nil_inv. eauto. subst. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia