proposition: Lemma evalDet_steps_done_support_singleton_h : forall (A : Set)(x1 x2 : comp_state A), evalDet_steps x1 x2 -> forall (c : Comp A) a s, x1 = (cs_more c nil) -> x2 = (cs_done a s) -> getSupport c = a :: nil.
proof: Proof. induction 1; intuition; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. assert (s0 = nil). eapply evalDet_step_done_nil_inv. eauto. subst. eapply evalDet_step_done_support_singleton. eauto. assert (s = nil). eapply evalDet_step_more_nil_inv. eauto. subst. assert (Permutation (getSupport c0) (getSupport c)). eapply evalDet_step_more_support_preserved. symmetry. eauto. assert (getSupport c = a :: nil). eapply IHevalDet_steps. eauto. eauto. rewrite H1 in H0. apply Permutation_sym in H0. apply Permutation_length_1_inv in H0. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia