proposition: Lemma evalDet_repeat_steps_more_inv_h : forall (A : Set)(x y : comp_state A) P, evalDet_repeat_steps P x y -> forall (c: Comp A)(P : A -> bool) s, y = (cs_more c s) -> False.
proof: Proof. induction 1; intuition; subst; try discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia