proposition: Lemma evalDet_step_done_support_singleton : forall (A : Set)(c : Comp A) s a, evalDet_step c s = cs_done a s -> getSupport c = (a :: nil).
proof: Proof. induction c; intuition; simpl in *. inversion H; clear H; subst. trivial. destruct (evalDet_step c s); discriminate. destruct (shiftOut s n). destruct p. discriminate. discriminate. discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia