proposition: Lemma evalDet_steps_nil_eq_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (c : Comp A)(a1 a2 : A) s2, x = (cs_more c nil) -> y = (cs_done a2 s2) -> In a1 (getSupport c) -> a1 = a2.
proof: Proof. induction 1; intuition; simpl in *; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. eapply evalDet_step_nil_inv; eauto. symmetry in H. specialize (evalDet_step_more_nil_inv _ H); intuition. subst. eapply IHevalDet_steps. eauto. eauto. eapply Permutation_in. eapply evalDet_step_more_support_preserved. eauto. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia