proposition: Lemma evalDet_steps_skipn : forall (A : Set)(c : Comp A)(a1 a2 : A) s1 s2, evalDet_steps (cs_more c s1) (cs_done a2 s2) -> In a1 (getSupport c) -> (a1 = a2 \/ (exists n, n > 0 /\ s2 = skipn n s1)).
proof: Proof. intuition. eapply evalDet_steps_skipn_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia