proposition: Lemma evalDet_step_done_val_eq : forall (A : Set)(c : Comp A)(a1 a2 : A) s1 s2, evalDet_step c s1 = (cs_done a2 s2) -> In a1 (getSupport c) -> a1 = a2.
proof: Proof. induction c; intuition; simpl in *. intuition; subst. inversion H; clear H; subst. trivial. destruct (evalDet_step c s1); discriminate. destruct (shiftOut s1 n); [ destruct p ; discriminate | discriminate ]. discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia